I'm wondering about a thing I noticed when reading the code of the guardedness checker in
filter_stack function goes into recursion (line 965 on the master branch) to filter the stack according to the remaining body
c0 of the match predicate with an altered environment
env, obtained at line 952. However, that environment will now contain the elements of the
ctx from decomposing the type
a, which I believe it shouldn't.
For example in:
Hypothesis (p : nat -> Prop). Hypothesis (H0 : forall n, p n -> p (S n)). Fixpoint test7 (n : nat) := fun H => match n return forall (H: forall m, p m), p n with | 0 => fun H => H 0 | S n => fun H => H0 n (test7 n H) end H.
When restricting the stack domain upon entering the match,
filter_stack will, in the first step, examine the prod
(H : forall m, p m). After decomposing the type
forall m, p m,
m will be added to
env in line 952. And now the remaining stack is restricted with
p n (by the recursive call) in an environment where the
Rel 2 for
n is incorrectly bound to
m, which shouldn't be in scope.
Can someone please confirm that this is unintended? (if so, the fix is simple: just rename the new env created in the
let in line 952 to not shadow the old one).
I've not really attempted to construct a more sophisticated example where this might actually break something (mostly because I don't fully understand why the restriction of subterm information flowing through a match is needed in the first place).
@Lennard Gäher you are right, I think this is unintended.
The filter_stack_domain ensures that the guard checking handles the "commutative cut" of iota and beta redexes correctly: one can consider
H a subterm in a branch
(match c with | Ci => fun H => b end) arg iff
arg is already a subterm of inductive type (and not arbitrary type). Failure to restrict this results in an inconsistency in presence of propositional extensionality or univalence (look for the coq-club messages and patches by Maxime Dénès IIRC)
Thanks for the confirmation and the pointers! I'll create an issue then.
(for reference, the corresponding thread on coq-club is https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html -- the restriction now makes a lot more sense to me).
Last updated: Oct 16 2021 at 02:03 UTC