Jason.v

From Coq Require Import 
Relation_Operators Utf8 Psatz Wf_nat.


Section Jason. 

  Context {A B : Type}
  (f : A * B -> nat).

  Theorem fn_acc : forall (n : nat) (au : A) (bu : B),
    f (au, bu) < n -> 
    Acc (fun '(xa, ya) '(xb, yb) => f (xa, ya) < f (xb, yb)) (au, bu).
  Proof.
    induction n as [| n IHn].
    +
      intros * Ha; nia.
    +
      intros * Ha.
      eapply Acc_intro;
      intros (ax, bx) Hb.
      eapply IHn.
      eapply PeanoNat.Nat.lt_le_trans;
      [exact Hb | nia].
  Qed.

  Theorem well_founded_fn : 
    well_founded (fun '(xa, ya) '(xb, yb) => f (xa, ya) < f (xb, yb)).
  Proof.
    intros (au, bu).
    apply (fn_acc (S (f (au, bu)))).
    nia.
  Defined.

End Jason.

Section Jason.
  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop.
  Variable leB : B -> B -> Prop.
  Variable fA : A -> nat. 
  Variable fB : B -> nat.
  Variable (hA : forall x y : A, (fA x) <= (fA y) -> leA x y).
 
  
  Lemma Acc_nat_wf : 
    forall (xu : A), Acc leA xu -> forall (yu : B), Acc leB yu -> 
      Acc (fun '(xa, ya) '(xb, yb) => 
      Nat.add (fA xa) (fB ya) < Nat.add (fA xb) (fB yb)) (xu, yu).
  Proof.
    refine(fix fn xu (accf : Acc leA xu) {struct accf} := 
      match accf with 
      | Acc_intro _ ha => _
      end).
    intros yu hb. 
    eapply fn;
    [eapply ha, hA | exact hb]; 
    nia.
  Defined.

  Lemma Wellfounded_custom_rel : 
    well_founded leA -> well_founded leB ->
    well_founded (fun '(xa, ya) '(xb, yb) => 
      Nat.add (fA xa) (fB ya) < Nat.add (fA xb) (fB yb)).
  Proof.
    unfold well_founded.
    intros ha hb (xu, yu).
    eapply Acc_nat_wf;
    [eapply ha | apply hb].
  Defined.

End Jason.