The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I just noticed that the standard library's
Wellfounded.Lexicographic_Product.wf_lexprod depends on the eq_rect_eq
axiom.  However, it's not very difficult to prove it without any
axioms:

Require Import Relation_Operators.
Require Import Transitive_Closure.

Section WfLexicographic_Product.
  Variable A : Type.
  Variable B : A -> Type.
  Variable leA : A -> A -> Prop.
  Variable leB : forall x:A, B x -> B x -> Prop.

  Notation LexProd := (lexprod A B leA leB).

  Lemma lexprod_inv_right : forall (x:A) (y:B x) (P : sigT B -> Prop),
    (forall (x':A) (y':B x'), leA x' x -> P (existT B x' y')) ->
    (forall y':B x, leB x y' y -> P (existT B x y')) ->
    forall pr:sigT B, LexProd pr (existT B x y) -> P pr.
  Proof.
    intros.
    revert H H0.
    refine (match H1 in (lexprod _ _ _ _ pr0 existT_x_y) return
      (let (x0, y0) return Prop := existT_x_y in
        (forall (x':A) (y':B x'), leA x' x0 -> P (existT B x' y')) ->
        (forall y':B x0, leB x0 y' y0 -> P (existT B x0 y')) -> P pr0) with
    | left_lex _ _ _ _ _ => _
    | right_lex _ _ _ _ => _
    end); auto.
  Qed.

  Lemma acc_A_B_lexprod :
    forall x:A,
      Acc leA x ->
      (forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
      forall y:B x, Acc (leB x) y -> Acc LexProd (existT B x y).
  Proof.
    induction 1; induction 2; constructor.
    inversion 1 using lexprod_inv_right; intros.

    apply H0; trivial.
    intros; apply H1; eauto using clos_trans.
    apply H1; eauto using clos_trans.

    auto.
  Qed.

  Theorem wf_lexprod :
    well_founded leA ->
    (forall x:A, well_founded (leB x)) -> well_founded LexProd.
  Proof.  (* unchanged from the standard library *)
    intros wfA wfB; unfold well_founded in |- *.
    destruct a.
    apply acc_A_B_lexprod; auto with sets; intros.
    red in wfB.
    auto with sets.
  Qed.

End WfLexicographic_Product.
-- 
Daniel Schepler