Stream: Coq users

Topic: Solving equations obligations


view this post on Zulip Notification Bot (Dec 13 2023 at 22:05):

Térence Clastres has marked this topic as unresolved.

view this post on Zulip Térence Clastres (Dec 13 2023 at 22:45):

I have to solve

(term_size arg < S (fold_left (fun (s : nat) (a : fsl_term) => s + term_size a) args 0))%nat

(this fold_left should allow me to prove this because it accumates the size of all the arguments and the 'arg' is part of 'args'.

Before the recursive call I I have something like this :
pattern matching on the recursive function main_f

[...] args with (f x) => {
   let res := fold_left (fun acc arg  =>
         main_f arg (*  <- rec call *)
   ) neutral args
}

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 23:12):

many of these problems can be solved by the inspect pattern — you can search this zulip/the repo for examples.

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 23:15):

Actually, hmm — that's a way to propagate equalities that are getting lost. But I can't tell if that's what's happening in your concrete program. What's the missing information for your goal?

view this post on Zulip Térence Clastres (Dec 13 2023 at 23:15):

Paolo Giarrusso said:

many of these problems can be solved by the inspect pattern — you can search this zulip/the repo for examples.

Thanks for your answer. While checking the examples I saw it but I didn't think it would apply to my issue since arg doesn't come from the (f x)

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 23:16):

Is the missing info that arg comes from args?

view this post on Zulip Térence Clastres (Dec 13 2023 at 23:16):

Paolo Giarrusso said:

Is the missing info that arg comes from args?

exactly

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 23:18):

I see the goal and the code share fold_left and args, but that's it — is args arg the same?

view this post on Zulip Térence Clastres (Dec 13 2023 at 23:23):

Paolo Giarrusso said:

I see the goal and the code share fold_left and args, but that's it — is args the same?

Sorry for the confusion, the fold_left in the goal is not the fold_left in the code it's part of the measure function I use for the term I recurse on. The fold_left is the code is a fold_left_2 I wrote which is just a fixpoint.

In the protoype code, args come from the term I pattern match on and is the same as the args I pass to fold_left_2. Thus, the arg my lambda get must be from args, but I don't see this information in the obligation.
Yes, the arg in the goal should be the same as the arg used in the code

Here is my fold_left_2 :

Fixpoint fold_left2 {Acc A B : Type} (f : Acc -> A -> B -> Acc) (acc:Acc) (l1 : list A) (l2 : list B) : Acc :=
    match l1,l2 with
      | nil,nil => acc
      | cons b1 t1,cons b2 t2 => fold_left2 f (f acc b1 b2) t1 t2
      | _,_ => acc (* both lists must have the same length,
       otherwise computation will be interrupted when one of the list is empty but not the other *)
end.

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 23:27):

Regardless: I think I've seen similar cases where I had to explicitly pass membership proofs during the recursion... But it's not an elegant solution, it's been a while, and I hope somebody has something better.

view this post on Zulip Paolo Giarrusso (Dec 13 2023 at 23:28):

I gotta go, but if possible, I'd recommend posting a self-contained example, instead of just selected snippets

view this post on Zulip Térence Clastres (Dec 13 2023 at 23:54):

Here is a somewhat minimal example of my issue :

  Require Import List.
  From Equations Require Import Equations.
  Set Equations Transparent.
  Set Universe Polymorphism.

  Import ListNotations.

  Import Sigma_Notations.

  Open Scope nat.

  Inductive term := T  | L (t: list term).

    Inductive ty : forall (A : Type) (P : A -> Type), Set :=
    | ty0 : ty term (fun _ => nat)
    | ty1 : ty term (fun _=> nat).

    Derive Signature NoConfusion for ty.

Fixpoint T_size (t:term) :nat := match t with
| T => 0
| L ts => List.fold_left (fun acc t => acc + (T_size t)) ts 1
end.

Equations measure : (Σ A P (_ : A), ty A P) ->  nat :=
    measure (_, _, a, ty0) =>  T_size a;
    measure (_, _, a, ty1) => T_size a.

Definition rel := Program.Wf.MR lt measure.

#[local] Instance: WellFounded rel.
Proof.
  red. apply Wf.measure_wf. apply Wf_nat.lt_wf.
Defined.

Definition pack {A} {P} (x : A) (t : ty A P) := (A, P, x, t) : (Σ A P (_ : A), ty A P).

Equations? double_fn {A} {P} (t : ty A P) (x : A) : P x by wf (pack x t) rel :=
  double_fn ty0 n := 3;
  double_fn ty1 T := 1;
  double_fn ty1 (L ts) := List.fold_left (fun ac arg => ac + (double_fn ty0 arg)) ts 0.
Proof.
 red. red. cbn.
 (* need info that arg is in ts *)
 (* I want to show that because arg is from ts, adding the size of all elements of ts and adding 1 is necessarly greater than the size of arg *)
Admitted.

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 01:36):

Indeed, one solution should be to write a variant of fold_left passing In arg args to its higher-order argument.

view this post on Zulip Térence Clastres (Dec 14 2023 at 01:40):

Ok, I'll do that. It's too bad there is no way to "expand" the context surrounding the recursive call.

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 01:44):

At least, I don't know a good one... In Agda you can use sized types for this, but the jury is out on whether that's a better idea.

view this post on Zulip Térence Clastres (Dec 14 2023 at 02:49):

So far I'm failing to write such a function...

view this post on Zulip Térence Clastres (Dec 14 2023 at 04:10):

I tried to do the following :

Definition fold_left_in {Acc A : Type} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc)   (acc:Acc)  : Acc.
Proof.
induction l as [|h t IH] eqn:L .
- exact acc.
- assert (Hl : List.In h (h::t)) by (now constructor).
    pose proof (f acc (exist _ h Hl)) as fres.
    (* need to use IH ...*)
    exact fres.
Defined.

But this doesn't work because I can't use the induction hypothesis...

view this post on Zulip Térence Clastres (Dec 14 2023 at 13:58):

2 other failed attempts :

The f passed to the recursive call is now supposed to be Acc -> {x : A | h = x \/ List.In x t} -> Accbut I can't construct it :

Equations? fold_left_in_bis {Acc A : Type} `{EqDec A} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc) (acc:Acc) : Acc :=
    | nil,_,acc => acc
    | cons h t,_,acc => fold_left_in_bis t _ (f acc (exist _ h _)).

Then I tried to use a nested call to keep the same f but then I need to solve h = h' \/ List.In h' t

Equations? fold_left_in_bis {Acc A : Type} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc) (acc:Acc) : Acc :=
| nil,_,acc => acc
| cons h t,_,acc => fold_left_in_bis_aux t  (f acc (exist _ h _))
    where fold_left_in_bis_aux : list A -> Acc -> Acc :=
        | nil,acc' => acc'
        | (cons h' t'),acc' => fold_left_in_bis_aux t' (f acc' (exist _ h' _))
        .

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 16:59):

what about this?

Fixpoint fold_left_in {Acc A : Type} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc)   (acc_base:Acc) {struct l} : Acc.
Proof.
destruct l as [|h t].
- exact acc_base.
- unshelve eapply (fold_left_in _ _ t _ (f acc_base (exist _ h _))).
    2: now constructor.
    intros acc_new [x Hxt].
    unshelve eapply (f acc_new (exist _ x _)).
    now constructor.
Defined.

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 16:59):

I'm in a hurry, so I'm not sure if this is fold_left

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 17:01):

however, given Acc -> {x : A | In x (h :: t)} -> Acc, it correctly constructs Acc -> {x : A | In x t} -> Acc by using In x t -> In x (h :: t), which I think is the key step.

view this post on Zulip Térence Clastres (Dec 14 2023 at 18:27):

Paolo Giarrusso said:

what about this?

Fixpoint fold_left_in {Acc A : Type} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc)   (acc_base:Acc) {struct l} : Acc.
Proof.
destruct l as [|h t].
- exact acc_base.
- unshelve eapply (fold_left_in _ _ t _ (f acc_base (exist _ h _))).
    2: now constructor.
    intros acc_new [x Hxt].
    unshelve eapply (f acc_new (exist _ x _)).
    now constructor.
Defined.

Very nice ! I took the liberty to dissect it and rewrite it my way so I can understand better what's going on, would you mind letting me know if my comments are correct ?

Fixpoint fold_left_in {Acc A : Type} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc)   (acc_base:Acc) {struct l} : Acc.
Proof.
destruct l as [|h t]; simpl in *.
- exact acc_base.
-
    (* call f on the head, store in acc_new*)
    unshelve epose proof (f acc_base (exist _ h _)) as acc_new; [now left|].
    (* do the recursive call on the tail with acc_new *)
    unshelve eapply (fold_left_in Acc A t _ acc_new).
    (* craft the function to handle the next recursive call *)
    intros acc_newnew [hh x].
    apply (f acc_newnew). split with hh. now right.
Defined.

view this post on Zulip Térence Clastres (Dec 14 2023 at 18:30):

Also, I had first tried using Fixpoint and do a proof on it as you did but I got an error message and forgot I have to manually specify on what argument is the structural recursion...
Would it have worked keeping it as a Definition and using induction on l to construct the function ?

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 20:49):

I think yes, it should be possible, but I was in a hurry and wanted to make it closer to the standard fold_left...

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 20:52):

Because running induction on lists essentially executes fold_right, I think that's a nontrivial exercise. Structural recursion is also (naturally) a fold_right, so I won't be surprised if this is still a right fold...

view this post on Zulip Paolo Giarrusso (Dec 14 2023 at 20:54):

Your comments look reasonable, but it'd probably be better to define this using refine and a proof term for extra clarity.

view this post on Zulip Térence Clastres (Dec 16 2023 at 16:29):

After minimizing as much as possible the issue, it doesn't look like it has anything to do with fold_left :

From Equations Require Import Equations.


Section test.
Require Import List.
  Set Equations Transparent.
  Set Universe Polymorphism.

  Import ListNotations.

  Import Sigma_Notations.

  Open Scope nat.

  Inductive term := T  | L (t: list term).

  Definition env_ty :Type := id -> option (list id *  term).

  Inductive ty : forall (A B  : Type), (A -> B -> Type) -> Set :=
    | f_a : ty env_ty term (fun  _ _ => nat)
    | f_b : ty env_ty  id (fun  _ _ =>  nat)
    .

    Derive Signature NoConfusion for ty.

    Fixpoint T_size (t:term) :nat := match t with
    | T => 0
    | L ts => List.fold_left (fun acc t => acc + (T_size t)) ts 1
    end.

    Equations measure : (Σ A B P (_ : A) (_ : B) , ty A B P) -> nat :=
        | (_,_,_, _,t,f_a) => T_size t
        | (_,_,_,_,_,f_b)  =>  0

.
Definition rel := Program.Wf.MR lt measure.

#[global] Instance: WellFounded rel.
Proof.
  red. apply Wf.measure_wf. apply Wf_nat.lt_wf.
Defined.

Definition pack {A B } {P} (x1 : A) (x2 : B) (t : ty A B P) :=
     (A,B,P, x1, x2, t) : (Σ A B  P (_ : A) (_ : B) , ty A B  P).

End test.
Equations mutrecf {A B} {P} (t : ty A B P) (a : A) (b : B)  : P a b   by wf (pack a b t) rel :=
| f_a , _, _  => 0
| f_b,env,fname with env fname =>
    {
        | Some (_,t) =>
            let neededsomehow := 0 in
            let reccall := mutrecf f_a env t in
            0
        | None =>  0
    }
.
Solve Obligations with red ;red ; cbn ; auto with arith.
Hypothesis fixme :forall b, (T_size b < 0)%nat.

Next Obligation. red. red. cbn. apply fixme. Qed.

view this post on Zulip Térence Clastres (Dec 16 2023 at 16:55):

As to why I need to write that :
In my real implementation, when f_a deals with a term which is a function call, it calls f_b, whose role is to decide if the original function should be specialized to one that is more efficient.
This is based on an other env, bind_env that adds extra information to the arguments used in the call.

f_bbegins by looking up the unspecialized function in env (this should always succeed).
It will then create a new specialized function if needed and add it to an extra env for specialized functions 'spec_env'. It is shared acrosse the two functions (not represented here)

The argument as to why the induction is correct :

Thus, spec_env has an upper bound.

I am however at loss on how to show that (create a custom well-founded relation ? ), hence the hypothesis.

view this post on Zulip Notification Bot (Dec 16 2023 at 16:55):

Paolo Giarrusso has marked this topic as unresolved.

view this post on Zulip Térence Clastres (Dec 16 2023 at 22:00):

Paolo Giarrusso said:

Your comments look reasonable, but it'd probably be better to define this using refine and a proof term for extra clarity.

Like that ?

Fixpoint fold_left_in {Acc A : Type} (l : list A) (f : Acc -> {x:A| List.In x l}  -> Acc)   (acc_base:Acc) {struct l} : Acc.
Proof.
    refine (match l with nil => fun _ => acc_base | cons h t => fun f => _ end f).
    refine (fold_left_in _ _ t _ (f acc_base (exist _ h _))).
    - refine (fun acc_new x => f acc_new (exist _ (proj1_sig x) _)). destruct x. simpl. now right.
    - now constructor.
Defined.

view this post on Zulip Térence Clastres (Dec 16 2023 at 22:59):

Another example of failure of proving functional induction :

From Equations Require Import Equations.
Section todo.
Set Equations Transparent.
Set Universe Polymorphism.

Definition M (T : Type) : Type := nat -> T * nat.

Definition bind {A B : Type} (m : M A) (f : A -> M B) : M B :=
    fun c =>  let (a, c') := m c in f a c'.

Inductive termA := T (p:termB) with termB := P.

Inductive ty : forall (A  : Type), (A  -> Type) -> Set :=
| f_a : ty  termB (fun _  => @state nat)
| f_b : ty  termA (fun _ => @state nat)
.
Derive Signature NoConfusion for ty.
Import Sigma_Notations.

Equations measure : (Σ A P (_ : A) , ty A P) -> nat :=
    | (_,_,p,f_a) => 0
    | (_,_,t,f_b) => 1
.

Definition rel := Program.Wf.MR lt measure.
#[global] Instance: WellFounded rel.
Proof.
    red. apply Wf.measure_wf. apply Wf_nat.lt_wf.
Defined.

Definition pack {A } {P} (x1 : A)  (t : ty A P) :=
     (A,P, x1, t) : (Σ A  P (_ : A) , ty A  P).
End todo.

Equations mutrec {A} {P} (t : ty A  P) (x: A) : P x  by wf (pack x t) rel :=

| f_a , _ => fun _ => (0,0)%nat
| f_b ,T p =>
    bind (fun _ => (0,0%nat)) (fun c =>
        let wut := "" in
        bind (mutrec f_a p) (fun _ =>
            fun _ => (0,0)%nat
        )
    )
.
Solve Obligations with red ;red ; cbn ; auto with arith.

view this post on Zulip Notification Bot (Dec 22 2023 at 16:54):

This topic was moved to #Equations devs & users > Solving equations obligations by Karl Palmskog.


Last updated: Jun 13 2024 at 19:02 UTC