Stream: Equations devs & users

Topic: cannot guess decreasing argument


view this post on Zulip walker (Apr 14 2023 at 14:47):

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

view this post on Zulip Matthieu Sozeau (Apr 14 2023 at 15:30):

It might be another case than rec/params where your definition is not structurally recursive

view this post on Zulip walker (Apr 14 2023 at 16:35):

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');
}.

view this post on Zulip walker (Apr 14 2023 at 16:36):

again this works with rename which takes (nat -> nat) but fails with subst which takes (nat -> Term)

view this post on Zulip Gaëtan Gilbert (Apr 14 2023 at 16:45):

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

view this post on Zulip Kenji Maillard (Apr 14 2023 at 17:15):

or you could add an explicit by struct t annotation

view this post on Zulip walker (Apr 14 2023 at 18:29):

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);

view this post on Zulip walker (Apr 14 2023 at 18:29):

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

view this post on Zulip walker (Apr 14 2023 at 18:31):

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

view this post on Zulip walker (Apr 14 2023 at 18:31):

note that the rename function is almost the same structure, ad there was no problems regarding being ill-formed.

view this post on Zulip walker (Apr 15 2023 at 11:06):

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

view this post on Zulip walker (Apr 15 2023 at 11:11):

also when I tried to use use the same map trick on subst instead of subst_params it was accepted, because the correct subst_paramwill be more complex than the one shown, and this is just the mimimum bug reproducer.

view this post on Zulip Gaëtan Gilbert (Apr 15 2023 at 11:30):

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;
}.

view this post on Zulip Gaëtan Gilbert (Apr 15 2023 at 11:31):

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 := ...

view this post on Zulip walker (Apr 15 2023 at 12:30):

so your suggestion worked, but I don't fully understand it

view this post on Zulip walker (Apr 15 2023 at 12:32):

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

view this post on Zulip walker (Apr 15 2023 at 12:32):

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 := ... not map = 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

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:37):

@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)

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:38):

it'd be nice if Coq were more liberal (and Agda is, but they have a _very_ different story for soundness)

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:39):

said otherwise, the recursion structure of your fixpoints must match closely the recursion structure of your inductives

view this post on Zulip walker (Apr 15 2023 at 12:40):

that would make sense, alright. my next question is, is there general pattern for dealing with nested induction ?

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:40):

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"

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:42):

but there's a second point about how map must be implemented, and I don't remember if that's explained there

view this post on Zulip walker (Apr 15 2023 at 12:42):

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.

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:42):

(I don't think so and I've never fully understood it — I've just seen it come up often)

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 12:44):

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

view this post on Zulip walker (Apr 15 2023 at 12:46):

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.

view this post on Zulip Gaëtan Gilbert (Apr 15 2023 at 12:49):

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

view this post on Zulip Gaëtan Gilbert (Apr 15 2023 at 12:53):

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

view this post on Zulip Gaëtan Gilbert (Apr 15 2023 at 12:55):

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

view this post on Zulip Matthieu Sozeau (Apr 17 2023 at 07:01):

You can use where instead of with for nested fixpoints

view this post on Zulip walker (Apr 17 2023 at 15:16):

I haven't tried it, but what will be the point of where if the two functions are no longer mutual?

view this post on Zulip Matthieu Sozeau (Apr 18 2023 at 17:04):

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.

view this post on Zulip walker (Apr 25 2023 at 08:06):

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

view this post on Zulip walker (Apr 25 2023 at 08:07):

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.

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:17):

Where is map_index_rev actually reversing the list? It seems just map_index?

view this post on Zulip walker (Apr 25 2023 at 08:24):

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 :(

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:24):

No the indexes are reversed, that's fine

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:26):

At least, you can prove the two versions are equivalent and then do the actual proofs on the nice version

view this post on Zulip walker (Apr 25 2023 at 08:26):

no I couldn't do that, but I can open a different thread for that

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:27):

Ah, you'd probably need to lift out the size computation

view this post on Zulip walker (Apr 25 2023 at 08:28):

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.

view this post on Zulip walker (Apr 25 2023 at 08:28):

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

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:30):

On your question: it's not clear that map (uncurry (rename ...)) is structurally recursive

view this post on Zulip walker (Apr 25 2023 at 08:32):

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?

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:33):

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

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:33):

Well! The problem for structural recursion is the zipping, and the problem for proofs is the size computation

view this post on Zulip walker (Apr 25 2023 at 08:34):

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

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:35):

That's not structural recursion. You can use well-founded induction but I'd try to avoid it here...

view this post on Zulip walker (Apr 25 2023 at 08:36):

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

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 08:37):

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

view this post on Zulip walker (Apr 25 2023 at 08:40):

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

view this post on Zulip walker (Apr 25 2023 at 08:42):

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.

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:02):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:03):

(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")

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:04):

(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)

view this post on Zulip walker (Apr 25 2023 at 09:19):

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 .

view this post on Zulip walker (Apr 25 2023 at 09:19):

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)

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:23):

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)

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:24):

So it is indeed more or less linked with the issue you describe

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:24):

And in theory we have lemmas relating the two notions of closedness, but in practice it is really frustrating to juggle between them

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 09:25):

what about doing rev (mapi f (rev l))?

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 09:27):

but would rev l be a subterm when l is?

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 09:30):

I guess not

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 09:38):

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