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