The Coq mailing list

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

Dear Suneel,

Thanks for your experiment with 'Equations' and your interest in the
Braga method.

Clearly, Equations makes an excellent job here and turns out to be the
quickest and most convenient approach, especially for a new coq user.
The Braga method has practical advantages in the following cases:
- the function you have in mind may "loop" on some inputs
  (so you have to find suitable additional arguments in order to ensure
   termination)
- even if the function always terminates, there is no clear suitable
  measure or well-founded relation 
  (see a good example in the thread recently started by Junyoung Clare
  Jang and Dominique Larchey-Wendling)
- you are interested in extracting the precise algorithm that you expect
  (whereas Equations introduces an additional layer).

A similarity between Equations and the Braga method is that a separate
description of the desired function is given, using respectively
recursive equations and an inductive relation in Prolog style
(e.g., Geither here).
The Coq function obtained in the two approaches automatically conforms
to the corresponding description. For the Braga method, this comes
from a basic use of the sig-type {r | Geither l1 l2 r} : up to the
management of this type, either_pwc is just a variant of the basic either0.

A more advanced usage of programming with dependent types was provided
for the projections πD1 and πD2. But please consider the version shown in
my previous message as an advanced exercise on "small inversions"
using dependent types, for my fun.
You can happily forget that and use Coq inversion tactic to automatically
program them as follows:

Let π𝔻2 {x1 x2 l1 l2} y2 (D : 𝔻ll (x1 :: l1) (x2 :: l2)) :
                𝔻ll l1 (y2 :: l2).
Proof. now inversion D. Defined.

On the conceptual side, the Braga methods only relies on bare Coq, on
top of which standard automated tactics (lia, inversion...) or
libraries (wf...) can be used at will as usual.

Regards,
Jean-François

On Wed, Aug 12, 2020 at 12:08:48PM +0530, Suneel Sarswat wrote:
>    Dear Jean-Francois,
>    Thanks for more information about the Braga method. I am yet to 
> understand
>    this method. An immediate benefit of Braga method over 'Equations' is 
> that
>    no additional installation is required. Also, as per the document, the
>    Braga method also works with non-terminating partial functions. But the
>    program, for a  new coq user like me, is much simpler in case of
>    Equations. Below is the solution to the same exercise I asked in the
>    original email, using 'Equations'. I am yet to discover the advantages of
>    one of the method over the other in reasoning involving compound Lemmas.
>    Any comments on this will be appreciated.
>    Regards,
>    Suneel
>    
> --------------------------------------------------------------------------------------------------
>    Require Import Lia.
>    Require Import Wf.
>    From Equations Require Import Equations.
>    Require Export Lists.List.
>    Equations either (l1:list nat) (l2: list nat) : (list nat) by wf (|l1| +
>    |l2|) :=
>      either nil _ := nil;
>      either _ nil := nil;
>      either (a1::l1') (a2 :: l2') := if (Nat.leb a1 a2) then a1::either l1'
>    ((a2 -a1)::l2') else a2::either ((a1-a2)::l1') l2'.
>      Next Obligation. lia. Qed.
> 
>    Lemma trivial1 (d:nat) (l1: list nat) (l2: list nat): (hd d (either l1
>    l2)) = (hd d l1)\/(hd d (either l1 l2)) = (hd d l2).
>    Proof. simpl. induction l1 as [| a1 l1']. left. auto. case l2 as [|a2
>    l2']. right. auto.
>    destruct (Nat.leb a1 a2) eqn:H1. left. simp either. rewrite H1. auto. 
> simp
>    either. rewrite H1. auto. Qed.
>    On Wed, Aug 12, 2020 at 3:31 AM Jean-Francois Monin
>    <[1]jean-francois.monin AT univ-grenoble-alpes.fr> wrote:
> 
>      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][2]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][3]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.