The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

I am trying to understand this proof [1]. It is very difficult to
understand by replaying the proof so I decided to write a custom
induction principle (le_pair_ind) which would make the proof trivial
and easier to read. However, I am stuck with a pattern in le_pair_ind.
In le_pair_ind, the first pattern, on l,  is fine but the problem
arises in the second pattern match, on h. I don't know how to force h
to be le_n. Any help would be appreciated.



Lemma le_pair_ind :
    forall (n : nat)
    (P : forall m : nat, n <= m -> n <= m -> Prop),
    P n (le_n n) (le_n n) ->
    (forall (m : nat) (l h : n <= m), P m l h ->
      P (S m) (le_S n m l) (le_S n m h)) ->
    forall (m : nat) (l h : n <= m), P m l h.
  Proof.
    intros ? P Hb Hc.
    refine(
      fix Fn m l :=
      match l as lp in (_ <= mp) return forall h, P mp lp h with
      | le_n _  => fun h => _ (* I DON'T KNOW HOW TO FORCE h  TO BE le_n *)
      | le_S _ m lp => _
      end).
  Admitted.

  Lemma le_unique : forall {m n : nat}
    (p q : m <= n), p = q.
  Proof.
    intros ? ? ? ?.
    apply (le_pair_ind m
      (fun (n : nat) (a : m <= n) (b : m <= n) => a = b)).
    + exact eq_refl.
    + intros ? ? ? He;
      subst; reflexivity.
  Qed.

Best,
Mukesh

[1] https://github.com/coq/coq/blob/master/theories/Arith/Peano_dec.v#L40