The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 9 janv. 2014, at 00:41, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:

> 
> On Jan 8, 2014, at 6:39 PM, Matthieu Sozeau 
> <matthieu.sozeau AT gmail.com>
>  wrote:
> 
>> Well, take the transitive closure of p <_le le_succ n m p.
>> — Matthieu
> 
> What is "p <_le le_succ n m p." ? 

I guess that was a bit short indeed :) Here are the details. I’m using 
packing with sigmas as it’s simpler to define the transitive closure 
once and for all for homogeneous relations, there might be a more clever 
way avoiding this:

I’m using Coq’s le in Prop, so I can’t prove wellfoundedness (this would 
contradict the proof-irrelevance principle that Coq enforces). But with
everything in Set the proof would go through.

<<
Require Import Relation_Definitions.
Require Import Relation_Operators.
Require Import Transitive_Closure.

Scheme le_dep := Induction for le Sort Prop.

(* That's <_le *)

Inductive le_le : forall {n m n' m' : nat}, le n m -> le n' m' -> Prop :=
  le_le_S : forall n m (p : le n m), le_le p (le_S _ _ p). 

Definition relation A := A -> A -> Prop.

Definition le_hom : relation {n : nat & { m : nat & le n m }} :=
  fun x y =>
    let 'existT n (existT m p) := x in
    let 'existT n' (existT m' p') := y in
      le_le p p'.

Definition le_rel : relation {n : nat & { m : nat & le n m }} :=
  clos_trans _ le_hom.

Require Import Program.
Goal forall x, Acc le_rel x.
Proof.
  intros x. apply Acc_clos_trans.
  destruct x as [n [m p]].
  simpl. induction p using le_dep. constructor.
  intros [n' [m' p']]. simpl.
  intros. (* inversion H does not close this branch as we are in Prop and 
le_n can't be
           discriminated from le_S *) admit.
  constructor.
  intros [n' [m' p']]. simpl.
  intros. 
  (* inversion H fails again as we are in Prop, but we should now that
      n = n', m = m' and p = p' and apply the induction hypothesis *)
  admit.
Qed.

>>

Now you can (virtually, if you redo this in Set) make a “mathematical" 
induction 
on derivations of [le], you just need to pack/curry the derivation with its 
indices
and apply the well-founded induction principle using the above proof.
— Matthieu