So I am trying to add inductive types to my toy language, and the constructor for recursor looks as follows:
Inductive Term : Type :=
| var (idx: nat): Term
...
...
| rec
(* name of the inductive type we are recursing on *)
(n: string)
(params: seq Term)
(* output type of the recursion branch *)
(C: Term)
(* what do to for every constructor*)
(branches: seq Term)
(* the main argument to provide to the rec function *)
(arg: Term).
The problem is that any recursive function has to also recurse over params
and branches
as well, and many o them fail for arbitrary reasons:
I was able to define a length function which simply counts nodes:
Equations term_nodes (t: Term) : nat := {
term_nodes (var _) := 1;
...
term_nodes (rec _ p c b a) := 1 + (sumn (map term_nodes p)) + term_nodes c + (sumn (map term_nodes b)) + term_nodes a
}.
Definition term_lt t1 t2 : Prop := term_nodes t1 < term_nodes t2.
Then I could do something like:
Equations rename (ξ : nat -> nat) (t: Term): Term := {
rename ξ (var idx) := var (ξ idx);
...
...
rename ξ (rec n p c b a) := let ξ' := uprenn ξ (length p) in
rec n (rename_params ξ p)
(rename ξ' c)
(rename_branches ξ' b)
(rename ξ a);
}
where rename_params (ξ: nat -> nat) (s: seq Term) : seq Term := {
rename_params ξ [::] := [::];
rename_params ξ (t::s') := (rename (uprenn ξ (length s')) t) :: (rename_params ξ s');
}
where rename_branches (ξ: nat -> nat) (s: seq Term) : seq Term := {
rename_branches ξ [::] := [::];
rename_branches ξ (t::s') := (rename ξ t):: rename_branches ξ s'
}.
Which works perfectly, and coq can actually see that everything is structurally decreasing, but when I do a similar function
Equations subst (σ: nat -> Term) (t: Term) : Term := {
subst σ (var idx) := σ idx;
...
...
subst σ (rec n p c b a) := rec n (subst_params σ p) c b a;
}
with subst_params (σ: nat -> Term) (s: seq Term) : seq Term := {
subst_params σ [::] := [::];
subst_params σ (t'::s') := (subst σ t')::(subst_params σ s');
}.
Coq gives:
Error: Cannot guess decreasing argument of fix.
It is not clear what is the problem, I tried using
Equations subst (σ: nat -> Term) (t: Term) : Term by wf t term_lt
and I get the error: Error: Mutual well-founded definitions are not supported
So my question is how can I just get this to work ?
Also, I am worried that if writing code is hard, then writing proofs is even harder so any general tips will also be appreciated
It might be another case than rec/params where your definition is not structurally recursive
this is not possible, the other cases are simple and they always worked and I never had to make any changes to them,
Let me show it here:
Equations subst (σ: nat -> Term) (t: Term) : Term := {
subst σ (var idx) := σ idx;
subst σ (univ l) := univ l;
subst σ (pi A B) := pi (subst σ A) (subst (up σ) B);
subst σ (lam y) := lam (subst (up σ) y);
subst σ (appl m n) := appl (subst σ m) (subst σ n);
subst σ (sigma A B) := sigma (subst σ A) (subst (up σ) B);
subst σ (pair m n) := pair (subst σ m) (subst σ n);
subst σ (proj1 m) := proj1 (subst σ m);
subst σ (proj2 m) := proj2 (subst σ m);
subst σ (gvar t) := gvar t;
subst σ (induct t) := induct t;
subst σ (constr t) := constr t;
subst σ (rec n p c b a) := rec n (subst_params σ p) c b a;
}
with subst_params (σ: nat -> Term) (s: seq Term) : seq Term := {
subst_params σ [::] := [::];
subst_params σ (t'::s') := (subst σ t')::(subst_params σ s');
}.
again this works with rename which takes (nat -> nat)
but fails with subst which takes (nat -> Term)
if you use a section like
Section S.
Variable (σ: nat -> Term).
Equations subst (t: Term) : Term := {
subst (var idx) := σ idx;
...
the error might be more explicit, because there is only 1 argument so there is no guessing about which might be the structural argument
or you could add an explicit by struct t
annotation
Gaëtan Gilbert said:
if you use a section like
Section S. Variable (σ: nat -> Term). Equations subst (t: Term) : Term := { subst (var idx) := σ idx; ...
the error might be more explicit, because there is only 1 argument so there is no guessing about which might be the structural argument
I am not sure if that will work, As you see there cases where \sigma
is not passed as is as in subst σ (sigma A B) := sigma (subst σ A) (subst (up σ) B);
Kenji Maillard said:
or you could add an explicit
by struct t
annotation
I did that as follows:
Equations subst (σ: nat -> Term) (t: Term) : Term by struct t := {
subst σ (var idx) := σ idx;
subst σ (univ l) := univ l;
subst σ (pi A B) := pi (subst σ A) (subst (up σ) B);
subst σ (lam y) := lam (subst (up σ) y);
subst σ (appl m n) := appl (subst σ m) (subst σ n);
subst σ (sigma A B) := sigma (subst σ A) (subst (up σ) B);
subst σ (pair m n) := pair (subst σ m) (subst σ n);
subst σ (proj1 m) := proj1 (subst σ m);
subst σ (proj2 m) := proj2 (subst σ m);
subst σ (gvar t) := gvar t;
subst σ (induct t) := induct t;
subst σ (constr t) := constr t;
subst σ (rec n p c b a) := rec n (subst_params σ p) c b a;
}
with subst_params (σ: nat -> Term) (s: seq Term) : seq Term by struct s := {
subst_params σ [::] := [::];
subst_params σ (t'::s') := (subst σ t')::(subst_params σ s');
}.
And now I get the full error:
Error: Recursive definition of subst_params is ill-formed.
In environment
subst : (nat -> Term) -> Term -> Term
subst_params : (nat -> Term) -> seq Term -> seq Term
σ : nat -> Term
s : seq Term
t : Term
l : seq Term
Recursive call to subst has principal argument equal to
"t" instead of "l".
Recursive definition is:
"fun (σ : nat -> Term) (s : seq Term) =>
match s with
| [::] => [::]
| t :: l => subst σ t :: subst_params σ l
end".
I am not sure what the problem is, it says subst
is recusing over t
instead of l
and apparently this is a problem here
note that the rename function is almost the same structure, ad there was no problems regarding being ill-formed.
what is truly puzzling me, is that all functions are working except for this subst function:
I created a function:
Equations term_nodes (t: Term) : nat := {
term_nodes (var _) := 1;
term_nodes (univ _) := 1;
term_nodes (pi A B) := 1 + term_nodes A + term_nodes B;
term_nodes (lam y) := 1 + term_nodes y;
term_nodes (appl m n) := 1 + term_nodes m + term_nodes n;
term_nodes (sigma A B) := 1 + term_nodes A + term_nodes B;
term_nodes (pair m n) := 1 + term_nodes m + term_nodes n;
term_nodes (proj1 m) := 1 + term_nodes m;
term_nodes (proj2 m) := 1 + term_nodes m;
term_nodes (gvar _) := 1;
term_nodes (induct _) := 1;
term_nodes (constr _) := 1;
term_nodes (rec _ p c b a) := 1 + (sumn (map term_nodes p)) + term_nodes c + (sumn (map term_nodes b)) + term_nodes a
}.
Which is almost the same structure for recursion and I tried to show that this is the thing structurally decreasing on every recursive call, but coq Equations is does not support wf for mutual recursion as in subst
also when I tried to use use the same map
trick on subst
instead of subst_params
it was accepted, because the correct subst_param
will be more complex than the one shown, and this is just the mimimum bug reproducer.
I guess mutual fixpoint doesn't work well with nested types, instead you need separately defined fixpoints
you may have to define subst_params first with an abstract subst
, ie
Section S.
(* IIRC the "subst" argument needs to be a lambda not a fix argument *)
Variable (subst : (nat -> Term) -> Term -> Term).
Equations subst_params (σ: nat -> Term) (s: seq Term) : seq Term by struct s := {
subst_params σ [::] := [::];
subst_params σ (t'::s') := (subst σ t')::(subst_params σ s');
}.
End S.
Equations subst (σ: nat -> Term) (t: Term) : Term by struct t := {
...
subst σ (rec n p c b a) := rec n (subst_params subst σ p) c b a;
}.
this is basically how map
works, its function argument is a lambda not fix argument iemap = fun A B f => fix map l := ...
not map = fix map A B f l := ...
so your suggestion worked, but I don't fully understand it
so I kept making small modifications till it get broken, and this is the last version that works:
Section SubstBranch.
Variable subst : (nat -> Term) -> Term -> Term.
Fixpoint map_rev_index (σ: nat -> Term) (s: seq Term) : seq Term :=
match s with
| [::] => [::]
| t::s' => let l := size s' in
(subst (upn l σ) t)::map_rev_index σ s'
end.
End SubstBranch.
Equations subst (σ: nat -> Term) (t: Term) : Term := {
subst σ (var idx) := σ idx;
subst σ (univ l) := univ l;
subst σ (pi A B) := pi (subst σ A) (subst (up σ) B);
subst σ (lam y) := lam (subst (up σ) y);
subst σ (appl m n) := appl (subst σ m) (subst σ n);
subst σ (sigma A B) := sigma (subst σ A) (subst (up σ) B);
subst σ (pair m n) := pair (subst σ m) (subst σ n);
subst σ (proj1 m) := proj1 (subst σ m);
subst σ (proj2 m) := proj2 (subst σ m);
subst σ (gvar t) := gvar t;
subst σ (induct t) := induct t;
subst σ (constr t) := constr t;
subst σ (rec n p c b a) := let σ' := upn (length p) σ in
rec n (map_rev_index subst σ p)
(subst σ' c)
(map (subst σ') b)
(subst σ a);
}.
Which is exactly what I want, but I make this tiny modification to the branch function:
Fixpoint map_rev_index (subst : (nat -> Term) -> Term -> Term) (σ: nat -> Term) (s: seq Term) : seq Term :=
match s with
| [::] => [::]
| t::s' => let l := size s' in
(subst (upn l σ) t)::map_rev_index subst σ s'
end.
I get the exact same error of "cannot figure the decreasing argument of fix" for in the real subst
equation
Gaëtan Gilbert said:
this is basically how
map
works, its function argument is a lambda not fix argument iemap = fun A B f => fix map l := ...
notmap = fix map A B f l := ...
I guess it has something to do with this but I don't understand what you are trying to say
@walker Fixpoint foo with bar
can _only_ consume types defined as Inductive foo with bar
(mutual inductives), _not_ Inductive foo := ... seq foo
(EDIT: that's what's called a nested inductive)
it'd be nice if Coq were more liberal (and Agda is, but they have a _very_ different story for soundness)
said otherwise, the recursion structure of your fixpoints must match closely the recursion structure of your inductives
that would make sense, alright. my next question is, is there general pattern for dealing with nested induction ?
yes! for a more extensive explanation, my favorite Google query is "cpdt coq nested inductive", which leads to http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html; look at "Nested Inductive Types"
but there's a second point about how map
must be implemented, and I don't remember if that's explained there
I think I checked that book in the past and if I remember correctly, my conclusion was it was mostly creativity, but I will check it again.
(I don't think so and I've never fully understood it — I've just seen it come up often)
generally, I'd say creativity is the problem; being _less_ creative and following the inductive structure more closely is the fix. Since seq
is a separate parametric inductive, then functions on it (like map
or subst_params
) must be separate fixpoints
noted, I will reread this section again while keeping this in mind, to be honest I am scared how the proofs of type safety will end up looking like given that I was struggling with just basic functions.
there is a symmetry between how the inductives are defined and how the fixpoints are defined
with the inductives there the inside type which takes a parameter, and the outside type which instantiates the inside type's parameter with itself (ie with the outside type)
with the fixpoints the fixpoint for the inside type needs to take a "parametric" argument which will b instantiated with the fixpoint for the outside type, after reduction this produces something like fix outside_fix x := ... (fix inside_fix y := ... (outside_fix something) ...) ...
ie a nested fixpoint
importantly it does NOT produce fix outside_fix x := ... ((fix inside_fix f y := ...) outside_fix ...
, because the guard checking will not identify the f
argument and outside_fix
so it only sees that you are using the unapplied outside_fix
in some abstract way, which is not allowed
for a concrete example look at
Require Import List.
Inductive rose := Rose (_:list rose).
Fixpoint size r := let '(Rose l) := r in S (fold_left (fun acc r => acc + (size r)) l 0).
Eval cbv [size fold_left] in size.
and
Fixpoint bad_fold_left A B (f:A->B->A) l acc :=
match l with
| nil => acc
| x :: tl => bad_fold_left A B f tl (f acc x)
end.
Fail Fixpoint bad_size r := let '(Rose l) := r in S (bad_fold_left _ _ (fun acc r => acc + (bad_size r)) l 0).
Eval cbv [bad_fold_left] in (fun bad_size r => let '(Rose l) := r in S (bad_fold_left _ _ (fun acc r => acc + (bad_size r)) l 0)).
BTW I don't think this is necessarily a fundamental restriction, after all Coq does track that the r
in fun acc r =>
is related to l
it's just how it works currently
You can use where instead of with for nested fixpoints
I haven't tried it, but what will be the point of where
if the two functions are no longer mutual?
Equations lets you write them as if they were mutual but in reality you can think of the the where definition being expanded at each use, as required for nested fixpoints by Coq's kernel.
I think I will need more help here,
So here is the current progress:
I was able to define this function:
Section MapIndexRev.
Variable T U: Type.
Variable f: nat -> T -> U.
Fixpoint map_index_rev (s: seq T) : seq U :=
match s with
| [::] => [::]
| t::s' => let l := size s' in
(f l t)::map_index_rev s'
end.
it is decreasing on s
and I used it to create the following as previously described:
Section RenameParams.
Variable (rename: (nat -> nat) -> Term -> Term).
Definition map_rename_params (ξ: nat -> nat) (s: seq Term) : seq Term :=
map_index_rev (fun l t => (rename (uprenn l ξ) t)) s.
End RenameParams.
Equations rename (ξ : nat -> nat) (t: Term): Term := {
rename ξ (var idx) := var (ξ idx);
rename ξ (univ l) := univ l;
rename ξ (pi A B) => pi (rename ξ A) (rename (upren ξ) B);
...
...
rename ξ (rec n p c b a) := let ξ' := uprenn (size p) ξ in
rec n
(map_rename_params rename ξ p) (* The part that will act funny *)
(rename ξ' c)
(map (rename ξ') b)
(rename ξ a);
Now in A different Coq user thread I got an equivalent but nicer map_index_rev
implementation:
Section MapIndexRevParam.
Variable T U: Type.
Variable f: nat -> T -> U.
Definition map_index_rev_params (start count: nat) (s: seq T) :=
map (uncurry f) (zip (rev (iota start count)) s).
End MapIndexRevParam.
Section MapIndexRev.
Variable T U: Type.
Variable f: nat -> T -> U.
(* this one does not work with subst, and rename*)
Definition map_index_rev' (s: seq T) :=
map_index_rev_params f 0 (length s) s.
End MapIndexRev.
but when I use it in map_rename_params
no problem happens, But then problems appear in rename itself, first it cannot guess the decreasing argument, then I did Equations rename (ξ : nat -> nat) (t: Term): Term by struct t
and this was the error
In environment
rename : (nat -> nat) -> Term -> Term
ξ : nat -> nat
t : Term
n : String.string
params : seq Term
C : Term
branches : seq Term
arg : Term
ξ' := uprenn (size params) ξ : nat -> nat
ξ0 := ξ : nat -> nat
s := params : seq Term
s0 := s : seq Term
start := 0 : nat
finish := length s0 : nat
s1 := s0 : seq Term
map : seq (nat * Term) -> seq Term
s2 : seq (nat * Term)
x : nat * Term
s' : seq (nat * Term)
p := x : nat * Term
x0 : nat
y : Term
l := x0 : nat
t0 := y : Term
Recursive call to rename has principal argument equal
to "t0" instead of
one of the following variables: "params"
"C" "branches" "arg" "s" "s0"
"s1".
Recursive definition is:
"fun (ξ : nat -> nat) (t : Term) =>
match t with
| var idx => var (ξ idx)
| univ l => univ l
| pi A B => pi (rename ξ A) (rename (upren ξ) B)
| lam y => lam (rename (upren ξ) y)
| appl m n => appl (rename ξ m) (rename ξ n)
| sigma A B =>
sigma (rename ξ A) (rename (upren ξ) B)
| pair m n => pair (rename ξ m) (rename ξ n)
| proj1 m => proj1 (rename ξ m)
| proj2 m => proj2 (rename ξ m)
| gvar n => gvar n
| induct n => induct n
| constr n => constr n
| rec n params C branches arg =>
let ξ' := uprenn (size params) ξ in
rec n (map_rename_params rename ξ params)
(rename ξ' C) [seq rename ξ' i | i <- branches]
(rename ξ arg)
end".
So what makes map_index_rev
good function and what makes map_index_rev'
bad one from. My code feels a bit unstable, because modification to one place will lead to compiler errors in a completely different location
I was intending to just stick to map_index_rev
but writing proofs for this one is very hard, for instance, I cannot even figure the lemma for map_index_rev (s1 ++ s2)
but the version built with map, iota, zip it is easier.
Where is map_index_rev actually reversing the list? It seems just map_index?
Paolo Giarrusso said:
Where is map_index_rev actually reversing the list? It seems just map_index?
well in the first iteration of development, I must admit, I tried so many things and only this version was the one that made the fix checker happy, but it is very hard to prove anything about :(
No the indexes are reversed, that's fine
At least, you can prove the two versions are equivalent and then do the actual proofs on the nice version
no I couldn't do that, but I can open a different thread for that
Ah, you'd probably need to lift out the size computation
It feels not straight forward to show that the two implementations are equal, because It is not clear what I am doing induction on, forward induction gets stuck at some point, backwards induction get stuck at different point.
Paolo Giarrusso said:
Ah, you'd probably need to lift out the size computation
yes and it gets fuzzy from here, so I thought , perhaps not worth it
On your question: it's not clear that map (uncurry (rename ...)) is structurally recursive
yes as a I suspected, but what are my options, other than proving that both versions are equivalent, which I don't know how to do?
Instead of doing a recursive call on the sublist, you're zipping it and applying uncurry (rename ...)
to it... I'm not sure the termination checker can expose this is structurally recursive by reduction
Well! The problem for structural recursion is the zipping, and the problem for proofs is the size computation
is there a way to prove structural recursion manually in equations, like in program
? I mean I know it is not possible, but what is the closest alternative
That's not structural recursion. You can use well-founded induction but I'd try to avoid it here...
Paolo Giarrusso said:
That's not structural recursion. You can use well-founded induction but I'd try to avoid it here...
oh that is the by WF thing ... yeah I never understood it and never ever knew how to do it by myself for once
So one approach (untested) is to combine the working approaches in both cases: write a recursive function (like the one passing termination checking) and passes start and/or count like the well-behaved function... Sketch in 5 minutes
Paolo Giarrusso said:
So one approach (untested) is to combine the working approaches in both cases: write a recursive function (like the one passing termination checking) and passes start and/or count like the well-behaved function... Sketch in 5 minutes
I will think how to do it, because without iota + rev, I will have to do something similar to count -= 1
which was something I tried hard to avoid
at this point, the metacoq solution for this problem starts to feel nice (due to Meven):
Definition map_index_rev {A B : Type} (f : nat -> A -> B) (l : list A) : list B :=
mapi (fun n => f (length l - n)) 0 l.
the subtraction is ofcourse annoying but I guess it is the not that annoying when compared to dealing with unhappy termination checker.
Is there a fundamental reason why you need to present the list in this order? If you are going to be doing a lot of de Bruijn manipulations on your list (and it looks like you are), it is nice to present it in the direction that makes these manipulations the least painful
(Btw, when I referred to MetaCoq I meant mostly for the usage of mapi
, I believe we have very little length/subtraction yoga there, because we try and do things "in the right direction")
(And the one place I remember where we reverse lists around is a formalization nightmare and one where I wish I'll never have to get into again)
so this is in particular the parameter list for inductive types:
Inductive MyType (T : Type) (L: seq T).......
Then there is two directions here to store this list of T
and L
... the direction that makes subtitution work with out subtraction (that will be T::L::[::]
because then T
will be lifted zero times, and L
will be lifted once ...etc
But there is the direction that makes type checking natural which will be the other direction L::T::[::]
because than we can always pop elements from the left and we are still left with well formed context .
Tell me that this is the one case where you had to deal with subtraction (checking metacoq code base is still a bit hard for me because everything is extra generalized)
If I recall correctly, this is a situation where we have two notions of a "closed context", one of them where we see the context as an extension of another one and want to start it from one side (which would be T
in your example I think), and one where we want to see a context by itself and want to start from the other side (the one on which we add new types)
So it is indeed more or less linked with the issue you describe
And in theory we have lemmas relating the two notions of closedness, but in practice it is really frustrating to juggle between them
what about doing rev (mapi f (rev l))
?
but would rev l
be a subterm when l
is?
I guess not
how about
Definition map_index_rev T U (f : nat -> T -> U) s :=
snd (List.fold_right (fun x '(len, v) => let v' := f (S len) x in (S len, v' :: v)) (0, nil) s).
Last updated: Oct 13 2024 at 01:02 UTC