The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

Dear Suneel,

As the Braga method offers many variants, here is a version with
explicit (and reasonably small) terms, based on a custom inductive
domain and a lightweight reasoning on the call graph.
I chose to prove that the domain is total at the end, in
order to illustrate that you can reason on your function
without this knowledge (not a big deal in this case study of course).
The same could be done using wf, measures, etc.

(* Recursion on 2 inputs *)

Require Import Utf8 List.
Import ListNotations.

Section secll.

Variable A : Type.
Implicit Type l : list A.

Inductive 𝔻ll : list A → list A → Prop :=
| 𝔻n1 l2 : 𝔻ll [] l2
| 𝔻n2 l1 : 𝔻ll l1 []
| 𝔻cc {x1 l1 x2 l2} :
    (∀ y1, 𝔻ll (y1 :: l1) l2) →
    (∀ y2, 𝔻ll l1 (y2 :: l2)) →
    𝔻ll (x1 :: l1) (x2 :: l2)
.

Let shape l := match l with _::_ => True | _ => False end.

Let π𝔻1 {x1 x2 l1 l2} y1 (D : 𝔻ll (x1 :: l1) (x2 :: l2)) :
                𝔻ll (y1 :: l1) l2 :=
  match D in 𝔻ll xl1 xl2 return
    let l1 := match xl1 with x1::l1 => l1 | _ => l1 end in
    let l2 := match xl2 with x2::l2 => l2 | _ => l2 end in
    shape xl1 → shape xl2 → 𝔻ll (y1 :: l1) l2 with
  | 𝔻cc D1 D2 => λ G1 G2, D1 y1
  | 𝔻n1 l2 => λ G1 G2, match G1 with end
  | 𝔻n2 l1 => λ G1 G2, match G2 with end
  end I I.

Let π𝔻2 {x1 x2 l1 l2} y2 (D : 𝔻ll (x1 :: l1) (x2 :: l2)) :
                𝔻ll l1 (y2 :: l2) :=
  match D in 𝔻ll xl1 xl2 return
    let l1 := match xl1 with x1::l1 => l1 | _ => l1 end in
    let l2 := match xl2 with x2::l2 => l2 | _ => l2 end in
    shape xl1 → shape xl2 → 𝔻ll l1 (y2 :: l2) with
  | 𝔻cc D1 D2 => λ G1 G2, D2 y2
  | 𝔻n1 l2 => λ G1 G2, match G1 with end
  | 𝔻n2 l1 => λ G1 G2, match G2 with end
  end I I.

Section params.

  Variable f g : A → A → A.
  Variable test : A → A → bool.

  (* A direct definition can be given... *)
  Fixpoint either0 l1 l2 (D: 𝔻ll l1 l2) : list A :=
     match l1, l2 return 𝔻ll l1 l2 → _ with
     | [], _ => λ _, []
     | _, [] => λ _, []
     | a1::l1', a2::l2' => λ D,
       match test a1 a2 with
       | true  => a1 :: either0 l1' (f a1 a2 :: l2') (π𝔻2 (f a1 a2) D)
       | false => a2 :: either0 (g a1 a2 :: l1') l2' (π𝔻1 (g a1 a2) D)
       end
     end D.

   (* ... but is hardly usable for proofs *)

  Reserved Notation "x '∅' y '⟼' z" (at level 70).

  Inductive 𝔾either : list A → list A → list A → Prop :=
  | Gn1 l2 : [] ∅ l2 ⟼ []
  | Gn2 l1 : l1 ∅ [] ⟼ []
  | Gcct a1 l1' a2 l2' r :
      test a1 a2 = true → l1' ∅ (f a1 a2 :: l2') ⟼ r →
      a1::l1' ∅ a2::l2' ⟼ (a1 :: r)
  | Gccf a1 l1' a2 l2' r :
      test a1 a2 = false → (g a1 a2 :: l1') ∅ l2' ⟼ r →
      a1::l1' ∅ a2::l2' ⟼ (a2 :: r)
  where "x '∅' y '⟼' z" := (𝔾either x y z).
  
  Fixpoint either_pwc l1 l2 (D: 𝔻ll l1 l2) : {r | l1 ∅ l2 ⟼ r}.
  refine(
     match l1, l2 return 𝔻ll l1 l2 → _ with
     | [], _ => λ _, exist _ [] _
     | _, [] => λ _, exist _ [] _
     | a1::l1', a2::l2' => λ D,
       match test a1 a2 as b return test a1 a2 = b → _ with
       | true  => λ E,
         let (r, G) := either_pwc l1' (f a1 a2 :: l2') (π𝔻2 (f a1 a2) D) in
         exist _ (a1 :: r)  _
       | false => λ E,
         let (r, G) := either_pwc (g a1 a2 :: l1') l2' (π𝔻1 (g a1 a2) D) in
         exist _ (a2 :: r)  _
       end eq_refl
     end D); now constructor.
  Defined.

  Definition either l1 l2 D := proj1_sig (either_pwc l1 l2 D).

  Lemma either_spec l1 l2 D : l1 ∅ l2 ⟼ proj1_sig (either_pwc l1 l2 D).
  Proof. apply proj2_sig. Qed.

  Variable fake : A.
  Definition hd := hd fake.

  Lemma 𝔾either_hd l1 l2 r : l1 ∅ l2 ⟼ r → hd r = hd l1 \/ hd r = hd l2.
  Proof. destruct 1; tauto. Qed.

  Lemma either_hd l1 l2 D :
    hd (either l1 l2 D) = hd l1 \/ hd (either l1 l2 D) = hd l2.
  Proof. apply 𝔾either_hd, either_spec. Qed.

  End params. 

Fixpoint 𝔻ll_total l1 : ∀ l2, 𝔻ll l1 l2 :=
  match l1 with
  | [] => 𝔻n1
  | x1 :: l1 =>
    (fix loop x1 l2 := 
       match l2 with
       | [] => 𝔻n2 (x1 :: l1)
       | x2 :: l2 => 𝔻cc (λ y1, loop y1 l2) (λ y2, all_𝔻ll l1 (y2 :: l2))
       end) x1
  end.

End secll.




Best,
Jean-François



On Tue, Aug 11, 2020 at 11:02:27PM +0530, Suneel Sarswat wrote:
>    Dear Dominique,
>    Thank you very much. This is extremely helpful I am reading the tutorial
>    paper
>    [1]https://members.loria.fr/DLarchey/files/papers/the_braga_method.pdf. I
>    shall explore both Equation and Braga method for solving this kind of
>    problems.
>    Thanks again,
>    Suneel
>    On Tue, Aug 11, 2020 at 7:33 PM Dominique Larchey-Wendling
>    <[2]dominique.larchey-wendling AT loria.fr> wrote:
> 
>      Dear Suneel,
>      This is what you'd get following the Braga method.
>      Best,
>      Dominique Larchey-Wendling
>      ------------
>      Require Import Wellfounded List Arith Lia.
> 
>      Section measure2_rect.
> 
>        Variable (X Y : Type) (m : X -> Y -> nat) (P : X -> Y -> Type).
> 
>        Hypothesis F : (forall x y, (forall x' y', m x' y' < m x y -> P x' 
> y')
>      -> P x y).
> 
>        Arguments F : clear implicits.
> 
>        Let m' (c : X * Y) := match c with (x,y) => m x y end.
> 
>        Notation R := (fun c d => m' c < m' d).
>        Let Rwf : well_founded R.
>        Proof. apply wf_inverse_image with (f := m'), lt_wf. Qed.
> 
>        Definition measure2_rect x y : P x y :=
>          (fix loop x y (A : Acc R (x,y)) { struct A } :=
>            F x y (fun x' y' H' => loop x' y' (@Acc_inv _ _ _ A (_,_) H'))) _
>      _ (Rwf (_,_)).
> 
>      End measure2_rect.
> 
>      Tactic Notation "induction" "on" hyp(x) hyp(y) "as" ident(IH) "with"
>      "measure" uconstr(f) :=
>         pattern x, y; revert x y; apply measure2_rect with (m := fun x y =>
>      f); intros x y IH.
> 
>      Tactic Notation "bool" "discr" :=
>        match goal with | H: ?b = true, G: ?b = false |- _ => exfalso; now
>      rewrite H in G end.
> 
>      Section either.
>        (* the graph of the either function *)
> 
>        Reserved Notation "x 'ø' y '~~>' z" (at level 70).
> 
>        Inductive geither : list nat -> list nat -> list nat -> Prop :=
>          | in_ge_0 : forall l, nil ø l ~~> nil
>          | in_ge_1 : forall l, l ø nil ~~> nil
>          | in_ge_2 : forall x l y m r, Nat.leb x y = true
>                                     -> l ø (y-x)::m ~~> r
>                                     -> x::l ø y::m  ~~> x::r
>          | in_ge_3 : forall x l y m r, Nat.leb x y = false
>                                     -> (x-y)::l ø m ~~> r
>                                     -> x::l ø y::m  ~~> y::r
>        where "x 'ø' y '~~>' z" := (geither x y z).
>        (* geither is the graph of a (partial) function, ie it is
>      deterministic *)
> 
>        Fact geither_fun l m r s : l ø m ~~> r -> l ø m ~~> s -> r = s.
>        Proof.
>          intros H; revert H s.
>          induction 1; inversion 1; subst; auto; try bool discr; f_equal;
>      auto.
>        Qed.
>        (* either packed with conformity *)
> 
>        Definition either_pwc l m  : { r | l ø m ~~> r }.
>        Proof.
>          induction on l m as either with measure (length l+length m).
>          revert either; refine(
>            match l, m with
>              | nil  , _    => fun _ => exist _ nil _
>              | _    , nil  => fun _ => exist _ nil _
>              | x::l , y::m => fun either => match Nat.leb x y as b return
>      Nat.leb x y = b -> _ with
>                | true  => fun E => let (r,Hr) := either l ((y-x)::m) _ in
>      exist _ (x::r) _
>                | false => fun E => let (r,Hr) := either ((x-y)::l) m _ in
>      exist _ (y::r) _
>              end eq_refl
>            end); try (simpl; lia); constructor; auto.
>        Qed.
> 
>        Definition either l m := proj1_sig (either_pwc l m).
> 
>        Fact either_spec l m :l ø m ~~> either l m.
>        Proof. apply (proj2_sig _). Qed.
>        (* Fixpoints eqs are what you need to work with either *)
> 
>        Fact either_fix_0 m : either nil m = nil.
>        Proof. apply geither_fun with (1 := either_spec _ _); constructor.
>      Qed.
> 
>        Fact either_fix_1 l : either l nil = nil.
>        Proof. apply geither_fun with (1 := either_spec _ _); constructor.
>      Qed.
> 
>        Fact either_fix_2 x y l m : Nat.leb x y = true -> either (x::l) 
> (y::m)
>      = x::either l ((y-x)::m).
>        Proof. intros H. apply geither_fun with (1 := either_spec _ _);
>      constructor; auto; apply either_spec. Qed.
> 
>        Fact either_fix_3 x y l m : Nat.leb x y = false -> either (x::l)
>      (y::m) = y::either ((x-y)::l) m.
>        Proof. intros H. apply geither_fun with (1 := either_spec _ _);
>      constructor; auto; apply either_spec. Qed.
> 
>        Check hd.
> 
>        Lemma trivial1 d l1 l2 : hd d (either l1 l2) = hd d l1
>                              \/ hd d (either l1 l2) = hd d l2.
>        Proof.
>          revert l1 l2; intros [ | x l ] [ | y m ].
>          + rewrite either_fix_0; auto.
>          + rewrite either_fix_0; auto.
>          + rewrite either_fix_1; auto.
>          + case_eq (Nat.leb x y); intros E.
>            * rewrite either_fix_2; auto.
>            * rewrite either_fix_3; auto.
>        Qed.
> 
>      End either.
> 
>    
> ══════════════════════════════════════════════════════════════════════════
> 
>        De: "Suneel Sarswat" <[3]suneel.sarswat AT gmail.com>
>        À: "coq-club" <[4]coq-club AT inria.fr>
>        Envoyé: Mardi 11 Août 2020 09:56:41
>        Objet: Re: [Coq-Club] Program Fixpoint and a function involving two
>        lists
> 
>        Dear Yishuai,
>        Thanks for the quick response. I shall surely look into it. Besides
>        this, any info on Program Fixpoint and proofs involving them will be
>        of great help to me.
>        Regards,
>        Suneel
>        On Tue, Aug 11, 2020 at 1:18 PM Yishuai Li <[5]yishuai AT cis.upenn.edu>
>        wrote:
> 
>          Hi Suneel,
> 
>          I've asked a similar question before:
>          
> [6]https://coq.discourse.group/t/fixpoint-with-two-decreasing-arguments/544
>          Alternative solution are internal auxiliary fixpoint and Equations,
>          which are shown under that thread.
> 
>          Hope it helps,
>          Yishuai
> 
>          Suneel Sarswat <[7]suneel.sarswat AT gmail.com> 于2020年8月11日周二 上
>          午3:27写道：
>          >
>          > I am trying to write a function involving two lists. In each
>          iteration, one of the lists decreases strictly. The Fixpoint 
> doesn't
>          work so tried Program Fixpoint with the measure on the sum of the
>          length of the two lists. Here is a minimum working example
>          >
>          > Require Import Wf.
>          > Program Fixpoint either (l1:list nat) (l2: list nat) {measure
>          (|l1| + |l2|)}:=
>          > match (l1,l2) with
>          > |(nil, _) => nil
>          > |(_,nil) => nil
>          > |(a1::l1',a2::l2') => match (Nat.leb a1 a2) with
>          >   |true  => a1::either l1' ((a2 -a1)::l2')
>          >   |false => a2::either ((a1-a2)::l1') l2'
>          >   end
>          >   end.
>          >
>          > Next Obligation.
>          > simpl. omega. Qed.
>          >
>          > Lemma trivial1 (l1: list nat) (l2: list nat): (hd (either l1 l2))
>          = (hd l1)\/(hd (either l1 l2)) = (hd l2).
>          > Proof. simpl. induction l1 as [| a1 l1']. left. auto. case l2 as
>          [|a2 l2']. right. auto.
>          > destruct (Nat.leb a1 a2) eqn:H1. right. unfold either. unfold
>          either_func.
>          >
>          > After the last tactic, I got stuck. It gives me a huge goal which
>          let alone proving, I don't even understand.
>          > I tried finding this out on the internet. I got a post on stack
>          exchange regarding this but that is not working. I got an error
>          "fix_sub_eq_ext" not recognized when I run 'rewrite fix_sub_eq_ext'
>          as per the instruction on the post. Besides this, I also did not
>          understand how do these tactics work. Is there any tutorial or 
> paper
>          where I can learn more about Program Fixpoint related tactics with 
> a
>          lot of examples?
>          >
>          > Besides this, is there an alternative way to write functions
>          involving two or more lists where only one of them is strictly
>          decreasing in each iteration. And prove their properties.
>          >
>          > Thanks,
>          > Suneel
>          >
> 
> References
> 
>    Visible links
>    1. https://members.loria.fr/DLarchey/files/papers/the_braga_method.pdf
>    2. mailto:dominique.larchey-wendling AT loria.fr
>    3. mailto:suneel.sarswat AT gmail.com
>    4. mailto:coq-club AT inria.fr
>    5. mailto:yishuai AT cis.upenn.edu
>    6. 
> https://coq.discourse.group/t/fixpoint-with-two-decreasing-arguments/544
>    7. mailto:suneel.sarswat AT gmail.com

-- 
Jean-Francois Monin
Verimag
Universite Grenoble Alpes