The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

Hi,

> The problem comes down to showing that two proofs of (x<limit) are 
> equivalent.

If you "compile" the the inductive predicate "le" into a computational 
definition this becomes rather easy.

Fixpoint le (a b : nat) { struct a } : Prop :=
match a, b with
| S a, S b => le a b
| S _, O => False
| O, _ => True
end.

The proof is then:

Goal forall a b (p1 p2 : le a b), p1 = p2.
induction a; simpl; intros.
  exact(match p1 as p1', p2 as p2' return p1'=p2' with I,I => 
refl_equal _ end).
  destruct b.
    exact (False_ind _ p1).
    apply IHa.
Qed.

I would be happy to see practical or philosophical arguments against 
this approach:
What is the advantage of defining "le" inductively?

Best,

Roland