[Agda] new generalize feature, first version

[Peter Divianszky]

Arseniy, thanks for the pointers.

I checked them and indeed, 'generalize' and 'variable' in lean is quite 
similar.
They both allow to specify the type of the generalizable variables.

I think 'generalize' is strictly more powerful, because you can use 
holes inside the specified types like

generalize  any : _    -- possible in Lean
                        -- this is idris-style generalization?

generalize  A : Ty _    -- not possible/not documented in Lean



On 2018-03-31 14:19, Arseniy Alekseyev wrote:
> It's possible that I'm missing a key distinction, but this `generalize` 
> keyword sounds like it's exactly the same as `variable` keyword in lean.
> 
> These two pages give some (very simple) description:
> https://leanprover.github.io/reference/other_commands.html
> https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections
> 
> I don't know where to find a more in-depth explanation of how this works.
> 
> On 31 March 2018 at 10:58, Nils Anders Danielsson <nad at cse.gu.se 
> <mailto:nad at cse.gu.se>> wrote:
> 
>     On 2018-03-31 00:00, Peter Divianszky wrote:
> 
>           >>      {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
>           >>
>           >> [...]
>           >>
>           >>      {x : ⊤} (p : tt ≡ x) → p ≡ p
>           >
>           > These two types are definitionally equal.
> 
>         Right, I just wanted to be precise with naming.
>         The former is the current type signature and the latter is the
>         desired one.
> 
> 
>     There is no difference between these type signatures, even if you take
>     the names of implicit arguments into account. Agda sometimes prints type
>     signatures using the {x = y : A} notation in order to avoid issues
>     related to shadowing. Here is one example:
> 
>        F : (Set → Set) → Set₁
>        F G = {A : Set} → G A
> 
>        T : Set₁
>        T = {A : Set} → F (λ X → A → X)
> 
>     How should the normal form of T be printed? Agda prints
> 
>        {A : Set} {A = A₁ : Set} → A → A₁.
> 
>     Note that this notation is not parsed by Agda.
> 
>           > One property I did not bring up was that of stability. I
>         hope that we
>           > will not end up in a situation in which one can break lots
>         of code by,
>           > say, adding one variable name to a generalize block.
> 
>         My idea would be stable in this sense.
> 
> 
>     You presented the following example in your first message:
> 
>         For example,
> 
>         postulate
>             ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
> 
>         means
> 
>         postulate
>             ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
>                   → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
> 
> 
>     This suggested to me that if I replaced
> 
>        {Γ Δ Θ} : Con
> 
>     with
> 
>        {Γ whatever Δ Θ} : Con,
> 
>     then the type signature would change. However, I see now that your
>     example uses the names Σ and Ω which are not listed in any generalize
>     block. I tried your example myself, and this is what you actually end up
>     with:
> 
>        {Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
>        {σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
>        ((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
> 
>     The telescope contains /three/ implicit arguments all named Γ.
> 
>     (I'm not sure why the {x = y : A} notation is used for all the other
>     implicit arguments. My guess would be that it has something to do with
>     the implementation of generalize.)
> 
>     If you perform the change that I mentioned above, then you still end up
>     with the type signature above. Thus the type signature is stable under
>     this particular kind of change.
> 
>     After some experimentation I managed to figure out where the names in
>     the type signature come from. If I replace
> 
>        Sub : (Γ Δ : Con) → Set
> 
>     with
> 
>        Sub : (Γ Σ : Con) → Set,
> 
>     then I get a different type signature:
> 
>        {Γ = Γ₁ : Con} {Σ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
>        {σ = σ₁ : Sub Γ₁ Σ} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
>        ((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
> 
>     I still don't quite understand why you get one occurrence of Σ but three
>     occurrences of Γ. Does it depend on arbitrary choices made by the
>     unifier?
> 
>     Furthermore I'm not sure that it's a good idea to use names subject to
>     α-conversion (like Π-bound names) in a setting in which α-conversion is
>     not applicable (like in implicit Π binders).
> 
>     I tried to figure out what would happen if one of the bound names in the
>     type signature of Sub shadowed another name by parametrising the
>     module:
> 
>        module _ {Σ : Set} where
> 
>     However, this triggered some kind of error:
> 
>        meta var MetaId 48 was generalized
>        CallStack (from HasCallStack):
>          error, called at
>     src/full/Agda/TypeChecking/Rules/Term.hs:1580:86 in [...]
> 
>     -- 
>     /NAD
> 
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
>