[Hol-info] defining functions on equivalence classes

[Michael N. <Mic...@ni...>]

[Part of this discussion seems to have fallen off hol-info; thanks to
the Isabelle user who brought Rene's response to my attention.]

Rene Vestergaard writes:
 
> [...] More details can be found from my homepage
> (http://www.jaist.ac.jp/~vester/) under the headings primitive
> reasoning/proof theory, etc.. In particular, there are primitive
> proofs of everything from confluence to standardisation and the
> decidability of alpha-equivalence; the various presentations point
> out the substantial problems that are glossed over in informal
> approaches and that are likely to cause problems for Peter Homeier's
> programme. Please do not hesitate to ask for further info.

I have proved standardisation and the various obvious confluence
results for a type isomorphic to the one Peter Homeier mentioned.  

I have a type 'a term with "constructors":

  VAR : string -> 'a term
  CON : 'a -> 'a term
  APP : 'a term -> 'a term -> 'a term
  LAM : string -> 'a term -> 'a term

but where 

  LAM x (VAR x) = LAM y (VAR y)

I thus have the basic first order syntax quotiented up to
alpha-equivalence.  There is an accompanying structural induction
principle that I used for the majority of the proofs I performed by
induction on term structure.  (Some, including the standardisation
theorem itself, were done by induction on term size.  This is how
Barendregt proves it too.)

My proof of standardisation and the finite-ness of developments
followed Barendregt's chapter 11 as closely as possible.  I found that
the majority of the problems with this formalisation had little to do
with the nature of my underlying type and more to do with other
aspects of Barendregt's proof.

For example, Barendregt's type \Lambda'* of terms with weighted
variables is modelled as pairs of terms and maps from variable
occurrences to non-zero natural numbers.  (Section 11.2) Just
specifying what happens to the map component of such a pair when a
substitution occurs is a major pain.  Indeed, Barendregt never really
defines what a variable occurrence is.  All of this is necessary for
his proof of the well-foundedness of the \beta_0 relation. 

So, I agree that there are "substantial problems that are glossed over
in informal approaches".  But my experience suggests that these
problems have relatively little to do with the fact that there is a
quotiented type underneath.

Michael.

[There is a description of this work at
    http://web.rsise.anu.edu.au/~michaeln/pubs/merlin2003.pdf
]