Térence Clastres has marked this topic as unresolved.
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
}
many of these problems can be solved by the inspect pattern — you can search this zulip/the repo for examples.
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?
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)
Is the missing info that arg comes from args?
Paolo Giarrusso said:
Is the missing info that arg comes from args?
exactly
I see the goal and the code share fold_left and args, but that's it — is args arg the same?
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.
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.
I gotta go, but if possible, I'd recommend posting a selfcontained example, instead of just selected snippets
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.
Indeed, one solution should be to write a variant of fold_left passing In arg args
to its higherorder argument.
Ok, I'll do that. It's too bad there is no way to "expand" the context surrounding the recursive call.
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.
So far I'm failing to write such a function...
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...
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' _))
.
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.
I'm in a hurry, so I'm not sure if this is fold_left
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.
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.
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 ?
I think yes, it should be possible, but I was in a hurry and wanted to make it closer to the standard fold_left...
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...
Your comments look reasonable, but it'd probably be better to define this using refine and a proof term for extra clarity.
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.
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 :
spec_env
strictly increasesbind_env
Thus, spec_env has an upper bound.
I am however at loss on how to show that (create a custom wellfounded relation ? ), hence the hypothesis.
Paolo Giarrusso has marked this topic as unresolved.
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.
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.
This topic was moved to #Equations devs & users > Solving equations obligations by Karl Palmskog.
Last updated: Jun 13 2024 at 19:02 UTC