The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Ian,

Nice exercise on lexicographic product of which the well foundedness

is proved by nested inductions. I am not sure the suggested induction on

the length is the principle you want, but the below proof uses induction

on the length. It moreover does not require the elements of the list to

belong to nat. You only need a wf relation on these

(of which < : nat -> nat -> Prop is just an particular example).

Hope this helps,

Best,

Dominique

(**************************************************************)

(*   Copyright Dominique Larchey-Wendling [*]                 *)

(*                                                            *)

(*                             [*] Affiliation LORIA -- CNRS  *)

(**************************************************************)

(*      This file is distributed under the terms of the       *)

(*         CeCILL v2 FREER SOFTWARE LICENSE AGREEMENT         *)

(**************************************************************)

Require Import List Arith Wellfounded.

Import ListNotations.

Set Implicit Arguments.

Section measure_rect.

  Variable (X : Type) (m : X -> nat) (P : X -> Type).

  Hypothesis F : forall x, (forall y, m y < m x -> P y) -> P x.

  Definition measure_rect x : P x.

  Proof.

    cut (Acc (fun x y => m x < m y) x); [ revert x | ].

    + refine (

        fix loop x Dx := @F x (fun y Dy => loop y _)

      ).

      apply (Acc_inv Dx), Dy.

    + apply wf_inverse_image with (f := m), lt_wf.

  Qed.

End measure_rect.

Tactic Notation "induction" "on" hyp(x) "as" ident(IH) "with" "measure" uconstr(f) :=

  pattern x; revert x; apply measure_rect with (m := fun x => f); intros x IH.

Section less_than_wf.

  Variable (X : Type) (R : X -> X -> Prop) (Rwf : well_founded R).

  Reserved Notation "l '<lex' m" (at level 70).  (* for lexicographic product *)

  Reserved Notation "l '<<' m" (at level 70).    (* for less than *)

  Inductive lex : list X -> list X -> Prop :=

    | lex_skip x l m : l <lex m -> x::l <lex x::m

    | lex_cons x y l m : length l = length m -> R x y -> x::l <lex y::m

  where "l <lex m" := (lex l m).

  Fact lex_length l m : l <lex m -> length l = length m.

  Proof. induction 1; simpl; auto. Qed.

  Fact lex_cons_inv l m : 

          l <lex m 

       -> match m with

            | [] => False

            | y::m =>

            match l with

              | [] => False

              | x::l => x = y /\ lex l m 

                     \/ R x y /\ length l = length m

            end

          end.

  Proof. inversion 1; auto. Qed.

  (* Proof of Acc lex m by nested induction on:

       - induction the length of m (IHm)

       - if m = [] then finished (no l exists st l <lex [])

       - if m = x::m' then  

         * we know Acc lex m' (by IHm)

         * induction on x using Rfw

         * induction on (Acc lex m')

  *) 

  Theorem lex_wf : well_founded lex.

  Proof.

    intros m; induction on m as IHm with measure (length m).

    destruct m as [ | y m ].

    + constructor; intros l Hl; apply lex_cons_inv in Hl; easy.

    + revert m IHm.

      induction y as [ y IHy' ] using (well_founded_induction Rwf).

      intros m IHm.

      assert (Acc lex m) as Hm.

      1: apply IHm; simpl; auto.

      assert (forall x l, R x y -> length l = length m -> Acc lex (x::l)) as IHy.

      1: { intros x l Hx Hl; apply IHy'; auto.

           intros; apply IHm.

           simpl in *; rewrite <- Hl; auto. }

      clear IHy' IHm.

      revert Hm IHy.

      induction 1 as [ m Hm IHm ]; intros IHy.

      constructor; intros l Hl; apply lex_cons_inv in Hl.

      destruct l as [ | x l ]; try tauto.

      destruct Hl as [ (-> & Hl) | (Hx & Hl) ].

      * apply IHm; auto.

        apply lex_length in Hl as ->; auto.

      * apply IHy; auto.

  Qed.

  Inductive less_than : list X -> list X -> Prop :=

    | less_than_lt l m : length l < length m -> l << m

    | less_than_eq l m : lex l m -> l << m

  where "l << m" := (less_than l m).

  Fact less_than_inv l m : l << m -> length l < length m \/ lex l m.

  Proof. inversion 1; auto. Qed.

  Theorem less_than_wf : well_founded less_than.

  Proof.

    intros m.

    induction on m as IHm with measure (length m).

    revert IHm; generalize (lex_wf m).

    induction 1 as [ m Hm IHm ]; intros H.

    constructor; intros l Hl. 

    apply less_than_inv in Hl as [ Hl | Hl ].

    + apply H; auto.

    + apply IHm; auto.

      intros; apply H.

      now apply lex_length in Hl as <-.

  Qed.

  Section less_than_rect.

    Variable (P : list X -> Type)

             (HP : forall m, (forall l, length l < length m -> P l)

                          -> (forall l, lex l m -> P l)

                          -> P m).

    Corollary less_than_rect m : P m.

    Proof.

      induction m as [ m IHm ] using (well_founded_induction_type less_than_wf).

      apply HP; intros; apply IHm.

      + now constructor 1.

      + now constructor 2.

    Qed.

  

  End less_than_rect.

End less_than_wf.

---

De: "Ian Shillito" <Ian.Shillito AT anu.edu.au>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Jeudi 25 Novembre 2021 08:10:01
Objet: [Coq-Club] A well-order on lists of natural numbers

Hi all, 

Consider the "less than" relation << on lists of natural numbers defined by the following clauses (where l0 l1 : list nat):

1. If (length l0) < (length l1), then (l0 << l1)
2. If (length l0 = length l1 = n) for some (n : nat), then follow the usual lexicographic order on n-tuples.

I strongly believe that this is a well-order on lists of natural numbers. I am interested in this property as it should help reach a strong (transfinite?) induction principle like the following:

Theorem listnat_strong_inductionT:

forall P : list nat -> Type,

(forall l0 : list nat, (forall l1 : list nat, ((l1 << l0) -> P l1)) -> P l0) ->

forall l : list nat, P l.

​Has anyone ever tried to formalise such a relation? Any reference, comment, or advice is welcome. 

Best,

Ian Shillito