Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Propositions Guarding Iota Reduction
It is possible for the guard of a fix-point to be of a type inside
Prop rather than a type inside
Set. This can be still used in functions whose output type is in Set. In fact, this is used in well-founded recursion.
It is this situation where one may be forced to evaluate an object living in
Prop. This evaluation proves to the system that the guard is not a purely hypothetical object.
To be concrete, consider some function defined by well founded recursion inside the context
H:well_founded gt, which is equivalent to
H:forall n, Acc gt n.
set (F:=fun (x:nat) (f:forall y:nat, y > x -> nat) => (S (f (S x) (le_n (S x))))). set (P:=fun _:nat => nat). set (f:=Fix H P F)
Loosely speaking f(x) = 1 + f(x+1) and because we are assuming the
gt relation is well founded (which it isn't) this function is well defined. In this context we can ask Coq to compute this function.
Eval compute in (f 0)
The result is
(fix ...) 0 (H 0) : nat but the fix point does not evaluate further because the guard
H 0 is in normal form, but does not have a constructor.
One can try to push the evaluation onward by giving a few constructors (
Acc_intro) for the match to succeed on
set (H':=(fun z => (Acc_intro z (fun y _ => (Acc_intro y (fun x _ => (H x))))))). set (g:=Fix H' P F). Eval compute in (g 0).
H' is another proof that
gt is well founded, but this proof has some
Acc_intro inside to allow the computation to continue further. The result of the compute is
S (S (fix ...) 0 (H 3)) : nat. So one can get some finite number of recursions done, but in the end we always run into the assumption
H that cannot be evaluated further.
The important point is to notice that Coq needs to evaluate the expression
H', defined above, in order to get to the point where (H 3) stops the evaluation. This evaluation occurs even that
H' has type
well_founded gt which lives in
Goal well_founded gt->False. intros H. set (F:=fun (x:nat) (f:forall y:nat, y > x -> nat) => (S (f (S x) (le_n (S x))))). set (P:=fun _:nat => nat). set (f:=Fix H P F). Eval compute in (f 0). set (H':=(fun z => (Acc_intro z (fun y _ => (Acc_intro y (fun x _ => (H x))))))). set (g:=Fix H' P F). Eval compute in (g 0).