The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Stefan Monnier wrote:
> 
>> What to do?  We've seen the discussion of John Major equality in
>> CoqArt... is this our only hope, or is there a lighter way?
> 
> I see other people have already solved your problem, but to get back to
> the title of your email, I also wonder: wouldn't it be possible to
> strengthen the definitional equality so that your code is accepted
> as is.
> 
> It seems that what is required here is to extend CIC with the an η-rule
> for inductive definitions plus some kind of "match-associativity"
> (analogous to the let-associativity rule that says that
> 
>    let x₁ = let x₂ = e₁ in e₂ in e₃  ≡  let x₂ = e₁ in let x₁ = e₂ in e₃
> 
> assuming x₂∉fv(e₁)).
> 
> I.e.:
> 
>      swap (swap d)
>      ≡ match (match d with R => L | L => R end) with R => L | L => R end
>      ≡ match d with R => match L with R => L | L => R end
>                   | L => match R with R => L | L => R end
>        end
>      ≡ match d with R => R | L => L end
>      ≡ d
> 
> the first ≡ is by unfolding the definition, the second is by
> match-associativity, the third by the usual reduction rules, the fourth
> by η.
> 
> Since CIC's consistency is not broken by η applied to the function
> space, maybe it can also sustain η applied to the inductive
> definitions space (tho you'd probably get into trouble with the issue
> of the strong elimination of large inductive definitions).
> 
> OTOH, adding a form of match-associativity seems a lot more
> far-fetched :-(
> Too bad, because it would be handy in various circumstances.
> 
> 
>         Stefan
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

Just because it's vaguely related (to your η idea) and also interesting,
there is a paper about simply typed calculus with eta for 2 (aka bool or
Dir), http://www.cs.nott.ac.uk/~txa/publ/flops04.pdf

In that calculus the definitional equality f = f . f . f (and swap . swap =
id) holds, so now I wonder how to go about extending this to a full blown
dependent type theory?

-- 
View this message in context: 
http://www.nabble.com/Strengthening-the-definitional-equality-on-types--tp24816612p24833834.html
Sent from the Coq mailing list archive at Nabble.com.