Consider the situation described by the code below, wherein I have a "piecewise" function h behaving differently (like f, or like g) depending on some (decidable) property condition of its input (h is defined using case_eq). Assume that I can prove that a property is guaranteed of the image of any x after application of either of the partial functions f or g; I should be able to prove that the entire function h guarantees property using a simple case_eq proof, no? Yet the following code rejects the rewrite step:
Section Error.
Variables X Y : Type.
Variables n m : Y.
Variable condition : X -> bool.
Variable property : Y -> Prop.
Definition type1 (x : X) : Prop := condition x = true.
Definition type2 (x : X) : Prop := condition x = false.
Variable f : {x:X | type1 x} -> Y.
Variable g : {x:X | type2 x} -> Y.
Definition h : X -> Y. intro x. case_eq (condition x); intro.
- exact (f (exist type1 x H)).
- exact (g (exist type2 x H)).
Defined.
Hypothesis Hf : forall x, property (f x).
Hypothesis Hg : forall x, property (g x).
Theorem hRange : forall x, property (h x).
Proof. intro. case_eq (condition x); intro.
- unfold h. rewrite H.
with the error
Abstracting over the term "condition x" leads to a term
fun b : bool =>
property
((if b as b0 return (b = b0 -> Y)
then fun H0 : b = true => f (exist type1 x H0)
else fun H0 : b = false => g (exist type2 x H0)) eq_refl)
which is ill-typed.
Reason is: Illegal application:
The term "exist" of type "forall (A : Type) (P : A -> Prop) (x : A), P x -> {x : A | P x}"
cannot be applied to the terms
"X" : "Type"
"type1" : "X -> Prop"
"x" : "X"
"H0" : "b = true"
The 4th term has type "b = true" which should be coercible to "type1 x".
Of course, I wish it would eliminate the if clause, rewriting the goal to property (f (exist type1 x H)) but Coq doesn't like this. Why not?
I feel Coq wouldn't behave like this if the hypothesis generated by case_eq in the definition of h wasn't implicated in the result (in this case, I could've rewritten h with a match clause, and those cause me no issue. In the present situation, just assume that the hypothesis is crucial to constructing some "non-computational" part of either f x or g x, e.g. if Y is itself a sig-type). I've read other threads like this and this, but to the short extent that I understand them, they don't help me understand my situation.
This problem occurs when you try to destruct or rewrite all the occurrences of a subterm. Here, you've rewritten condition x in the type of H0, which causes exist type1 x H0 to be ill-typed (can you see why?).
The solution is to restrict the destruct or rewrite to only some of the subterms. This might require you to generalize part of your goal. For example:
From Coq Require Import ssreflect.
Section Error.
Variables X Y : Type.
Variables n m : Y.
Variable condition : X -> bool.
Variable property : Y -> Prop.
Definition type1 (x : X) : Prop := condition x = true.
Definition type2 (x : X) : Prop := condition x = false.
Variable f : {x:X | type1 x} -> Y.
Variable g : {x:X | type2 x} -> Y.
Definition h : X -> Y. intro x. case_eq (condition x); intro.
- exact (f (exist type1 x H)).
- exact (g (exist type2 x H)).
Defined.
Hypothesis Hf : forall x, property (f x).
Hypothesis Hg : forall x, property (g x).
Theorem hRange : forall x, property (h x).
Proof.
intro; unfold h; generalize (eq_refl (condition x)).
case: {2 3}(condition x).
- intros H. apply Hf.
- intros H. apply Hg.
Qed.
End Error.
After generalizing eq_refl, the goal looks like this:
1 subgoal (ID 16)
X, Y : Type
n, m : Y
condition : X -> bool
property : Y -> Prop
f : {x : X | type1 x} -> Y
g : {x : X | type2 x} -> Y
Hf : forall x : {x : X | type1 x}, property (f x)
Hg : forall x : {x : X | type2 x}, property (g x)
x : X
============================
forall e : condition x = condition x,
property
((if condition x as b return (condition x = b -> Y)
then fun H : condition x = true => f (exist type1 x H)
else fun H : condition x = false => g (exist type2 x H)) e)
The tactic case: {2 3}..., which was imported from ssreflect, says that condition x should only be destructed on the RHS of e and on the condition of the if.