[Agda] new generalize feature, first version

[Arseniy Alekseyev]

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> 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
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180331/e9ec76e2/attachment.html>