[Agda] new generalize feature, first version

[Andrés Sicard-Ramírez]

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).

-- 
Andrés