The Coq mailing list

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

Hi Jason,

I don't know if it is going to be any useful to you because it does not involve Equations but vanilla Coq [1, 3].  If you can find a function *f* that takes a pair of type A * B and returns a nat. You can use it for well-founded induction, and you either decrease on the first argument or  the first argument stays the same and you decrease on the second argument (structural recursion); in either case, the nat coming out of *f* decreases. You can also see [2] for more examples.

Best,

Mukesh

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.

(* This one simply falls back on well-foundedness of leA and leB *) 

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.

[1] https://gist.github.com/mukeshtiwari/382ba15f53bb979108c9436d9c402c13
[2] https://github.com/DmxLarchey/Accessibility/blob/main/acc.v
[3] https://github.com/coq/coq/blob/master/theories/Arith/Wf_nat.v

On Fri, Apr 19, 2024 at 8:15 PM Jason Hu <fdhzs2010 AT hotmail.com> wrote:

Hi,

Is there a way to use Equations to achieve something in one goal from the title? It is often needed when we can handle most cases using normal structural induction (keeping the same index), but then some special cases only decrease on some other index. Surely we can define a lexicographical order but I am hoping it can be voided.

Thanks,

Jason Hu

https://hustmphrrr.github.io/