## Stream: Coq users

### Topic: Solving equations obligations

#### Notification Bot (Dec 13 2023 at 22:05):

Térence Clastres has marked this topic as unresolved.

#### 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
}
``````

#### 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.

#### 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?

#### 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)`

#### Paolo Giarrusso (Dec 13 2023 at 23:16):

Is the missing info that arg comes from args?

#### Térence Clastres (Dec 13 2023 at 23:16):

Paolo Giarrusso said:

Is the missing info that arg comes from args?

exactly

#### 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?

#### 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.
``````

#### 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.

#### 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

#### 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 *)
``````

#### 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.

#### 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.

#### 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.

#### Térence Clastres (Dec 14 2023 at 02:49):

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

#### 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...

#### 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} -> Acc`but 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' _))
.
``````

#### Paolo Giarrusso (Dec 14 2023 at 16:59):

``````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.
``````

#### Paolo Giarrusso (Dec 14 2023 at 16:59):

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

#### 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.

#### Térence Clastres (Dec 14 2023 at 18:27):

Paolo Giarrusso said:

``````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.
``````

#### 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 ?

#### 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...

#### 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...

#### 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.

#### 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.
``````

#### 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_b`begins 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 :

• When we require generating a new function, `spec_env` strictly increases
• We assume a finite number of unspecialized functions to call
• For each unspecialized function, we assume a finite number of `bind_env`

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.

#### Notification Bot (Dec 16 2023 at 16:55):

Paolo Giarrusso has marked this topic as unresolved.

#### 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.
``````

#### 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.
``````

#### 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