The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

Meanwhile, when it comes to tinkering with the definitional
equality...

...be careful what you wish for.

On 5 Aug 2009, at 19:29, muad wrote:

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

It seems difficult to do this for inductive datatypes in general.
Somebody must know the status of eta-rules, commuting conversions,
and such like..? How badly do they break the decidability of
definitional equality? What happens with inductive families?

> 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?

Yeah, it's cute. It amounts to comparing the BDDs which express
the extensions of functions, if I recall correctly.

The general idea seems to be to improve the definitional equality
for functions from the precisely intensional by sampling them on
a finite covering of their inputs: picking the trivial covering
consisting of a fresh variable gives you the usual eta-law for
function spaces, but one could imagine constructing coverings
on a per-type basis. It would take some care to get this right,
in a suitably higher-order way. There's also a limitation with
empty types: extensionally, there's only one function in 0 -> 2,
but you may perfectly well give that type to (fun _ => true) and
(fun _ => false), and if you choose to identify them
definitionally, you collapse the definitional equality in nonempty
contexts.

Meanwhile, if we want to solve this particular problem,
not . not = id, by adjusting the definitional equality, there's
perhaps a cheap way. Suppose we have a primitive not, with
computation rules

  not true  --> false
  not false --> true

(defining not as a match does not break this trick but it increases
its price, unless you do the "labelled type" thing I wrote about
a while back). Suppose also that your conversion test is in two
phases: first, untyped beta-delta-iota reduction; second,
type-directed expansion to eta-long form. Modify the second
phase to simplify neutral terms of ground type, rewriting
(not (not n)) to n. Note that this n is necessarily neutral, hence
this simplification can never create a redex. It is easy to show
that extending the equational theory with (not (not n)) = n for
neutral n does, in fact, make (not (not t)) = t hold for any t.
This gives me some hope that the above procedure is complete to
decide the theory so extended, but to prove this conjecture is a
harder task, and I have not yet done so.

There's work to do here, but I think this may be yet another
Jagger/Richards situation, where you can't have the grand theory
extension of which the problem is a tiny special case, but you
can still solve the problem.

All the best

Conor