The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

Dear Dominique,

Thank you very much. This is extremely helpful I am reading the tutorial paper 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 <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" <suneel.sarswat AT gmail.com>
À: "coq-club" <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 <yishuai AT cis.upenn.edu> wrote:

Hi Suneel,

I've asked a similar question before:
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 <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
>