[Agda] new generalize feature, first version

[Peter Divianszky]

Andrés, thanks for the pointers.

Yes, it seems that Coq also has a forall-generalisation.
The main difference is that it is not possible to specify the types of 
the variables to be generalized.


On 2018-04-01 17:18, Andrés Sicard-Ramírez wrote:
> On 29 March 2018 at 07:13, Peter Divianszky <divipp at gmail.com> wrote:
>> Dear Agda users and implementors,
>>
>> I implemented a first version of forall-generalization, and I would like
>> to get feedback on it.
>>
>>
>> For users
>> ---------
>>
>> An example Agda file can be found at
>> https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
>>
>> Suppose that the following Set formers were postulated:
>>
>> postulate
>>    Con :                       Set
>>    Ty  : (Γ : Con) →           Set
>>    Sub : (Γ Δ : Con) →         Set
>>    Tm  : (Γ : Con)(A : Ty Γ) → Set
>>
>> There is a new keyword 'generalize', which accept declarations like
>> 'field' for records:
>>
>> generalize
>>    {Γ Δ Θ} : Con
>>    {A B C} : Ty _
>>    {σ δ ν} : Sub _ _
>>    {t u v} : Tm _ _
>>
>> After these 12 declarations
>>
>> (1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
>> forall-generalized, so, for example
>>
>> postulate
>>    id  : Sub Γ Γ
>>    _∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
>>
> 
> It seems that Coq also has a forall-generalisation mechanism (which
> I'm not familiarised).
> 
>    (* Tested with Coq 8.7.1. *)
> 
>    Require Import Unicode.Utf8.
> 
>    Axiom Con : Set.
>    Axiom Sub : Con → Con → Set.
> 
>    Generalizable All Variables.
>    Axiom id   : `{Sub Γ Γ}.
>    Axiom comp : `{Sub Θ Δ → Sub Γ Θ → Sub Γ Δ}.
> 
> 
> See Section 2.7.19 of
> https://github.com/coq/coq/releases/download/V8.7.2/coq-8.7.2-reference-manual.pdf
> (because Coq website ( https://coq.inria.fr/ ) seems down).
>