Musings.v

From Coq Require Import 
Relation_Operators Utf8 Psatz Wf_nat.


Section Morp.

  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop. (* A relation on type A *)
  Variable leB : B -> B -> Prop. (* A relation on type B *)
  Variable fA : A -> nat. (* A function from A to natural numbers *)
  Variable fB : B -> nat. (* A function from B to natural numbers *)
  Variable (hA : forall x y, leA x y <-> fA x < fA y).
  Variable (hB : forall x y, leB x y <-> fB x < fB y).


  Definition morphism_symprod_lt : 
    forall (ax bx : A) (au bu : B), 
    symprod A B leA leB (ax, au) (bx, bu) -> 
    (fA ax < fA bx ∧ au = bu) ∨ 
    (ax = bx ∧ fB au < fB bu).
  Proof.
    intros * Ha; 
    inversion Ha; subst;
    [left | right].
    +
      split;
      [eapply hA; assumption | reflexivity].
    +
      split;
      [reflexivity | eapply hB; assumption].
  Qed.


  Definition morphism_lt_sumprod : 
    forall (ax bx : A) (au bu : B),
    (fA ax < fA bx ∧ au = bu) ∨ (ax = bx ∧ fB au < fB bu) -> 
    symprod A B leA leB (ax, au) (bx, bu).
  Proof.
    intros * [(Ha & Hb) | (Ha & Hb)]; subst.
    +
      eapply left_sym, hA; assumption.
    +
      eapply right_sym, hB; assumption.
  Qed.

  Lemma Acc_symprod :
    forall xt : A, Acc leA xt -> forall yt : B, Acc leB yt -> 
    Acc (symprod A B leA leB) (xt, yt).
  Proof.
    induction 1 as [xt Ha Ihx].
    induction 1 as [yt Hb Ihy].
    eapply Acc_intro; intros (yu, yv) Hc.
    inversion Hc; subst.
    +
      eapply Ihx; try assumption.
      eapply Acc_intro; intros * Hd.
      eapply Hb; exact Hd.
    +
      eapply Ihy; assumption.
  Qed.


End Morp.
    

  


Section Jason. 

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

  Theorem fn_acc : forall (n : nat) (au : A) (bu : B),
    (* This theorem states that if f (au, bu) is less than n, then the pair (au, bu) is
       accessible in the relation defined by (fun '(xa, ya) '(xb, yb) => f (xa, ya) < f (xb, yb)). *)
    f (au, bu) < n -> 
    Acc (fun '(xa, ya) '(xb, yb) => f (xa, ya) < f (xb, yb)) (au, bu).
  Proof.
    (* The proof proceeds by induction on n. *)
    induction n as [| n IHn].
    +
      (* In the base case where n = 0, the goal is trivially true because
         there is no natural number less than 0. *)
      intros * Ha; nia.
    +
      (* In the inductive case, we assume the theorem holds for n and
         prove it for (S n). *)
      intros * Ha.
      eapply Acc_intro;
      (* We need to show that for any pair (ax, bx), if f (ax, bx) < f (au, bu),
         then (ax, bx) is accessible in the relation. *)
      intros (ax, bx) Hb.
      eapply IHn.
      (* We use the transitivity of < to show that f (ax, bx) < n,
         which allows us to apply the inductive hypothesis. *)
      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. (* A relation on type A *)
  Variable leB : B -> B -> Prop. (* A relation on type B *)
  Variable fA : A -> nat. (* A function from A to natural numbers *)
  Variable fB : B -> nat. (* A function from B to natural numbers *)
  Variable (hA : forall x y : A, (fA x) <= (fA y) -> leA x y). (* A property relating fA and leA *)
 
  
  Lemma Acc_nat_wf : 
    (* This lemma states that if xu is accessible in the relation leA, and yu is accessible in the relation leB,
       then the pair (xu, yu) is accessible in the relation defined by
       (fun '(xa, ya) '(xb, yb) => Nat.add (fA xa) (fB ya) < Nat.add (fA xb) (fB yb)). *)
    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.
    (* The proof proceeds by defining a recursive function fn using the fix tactic. *)
    refine(fix fn xu (accf : Acc leA xu) {struct accf} := 
      match accf with 
      | Acc_intro _ ha => _
      end).
    (* In the body of the function, we assume yu is accessible in leB, and show that (xu, yu) is accessible
       in the desired relation. *)
    intros yu hb. 
    (* We apply the recursive call fn to xu, using the accessibility evidence ha and the property hA
       to show that xu is accessible in leA. *)
    eapply fn;
    [eapply ha, hA | exact hb]; 
    (* Finally, we use the nia tactic to discharge the remaining goal. *)
    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.