I was trying to write a function whose type is forall n, option (n = 1).
I choose option as an altertnative to reflect avoiding giving the proof of the negative case. So Some plays the role ReflectT and holds the proof, while None doesn't hold the negative proof.
Definition is_1 n: bool:=
match n with
1 => true |
_ => false
end.
Lemma is_1_complete : forall n, is_1 n = true -> n = 1.
intros.
destruct n. simpl in H. discriminate.
destruct n. reflexivity.
simpl in H. discriminate.
Qed.
Lemma a_nat_is_1_or_not: forall n, option (n = 1).
intros.
cut (is_1 n = true -> n = 1).
-
intros.
destruct n. exact None.
destruct n. simpl in H. exact (Some (H (eq_refl))).
exact None.
-
exact (is_1_complete n).
Qed.
I've done with tactics. a_nat_is_1_or_not is the proof. And I thought I can do this writing the definition directly, so I tried.
Definition a_nat_is_1_or_not' n: option (n = 1) :=
match is_1 n with
true => Some (is_1_complete n eq_refl)
| false => None
end.
But Coq saids
Error:
In environment
n : nat
The term "eq_refl" has type "is_1 n = is_1 n"
while it is expected to have type "is_1 n = true" (cannot unify "is_1 n" and
"true").
It seems is_1 n cannot be unified to true in true case of the pattern matching of itself.
So I tried a more trivial example.
Definition every_true_is_I x: x = I :=
match x with
I => eq_refl
end.
It works.
What is the difference between a_nat_is_1_or_not' and every_truer_is_I?
Am I missing something? What can I do for writing a valid definition of forall n, is_1 n = true -> n = 1.?
The difference is that, in a_nat_is_1_or_not', you are depending on an external term whose type is is_1 n = true -> _. If you want a_nat_is_1_or_not' to look like every_true_is_I, you have to make sure that all the occurrences of is_1 n are covered by the pattern matching:
Definition a_nat_is_1_or_not' n: option (n = 1) :=
match is_1 n as b return ((b = true -> _) -> _) with
| true => fun H => Some (H eq_refl)
| false => fun _ => None
end (is_1_complete n).
Notice how is_1_complete has been instantiated outside the pattern matching, so that its occurrence of is_1 n (renamed b) is handled.
There is another way to do it, perhaps a bit more idiomatic. Instead of generalizing the whole context, you just keep enough information to fill all the holes:
Definition a_nat_is_1_or_not' n: option (n = 1) :=
match is_1 n as b return (is_1 n = b -> _) with
| true => fun H => Some (is_1_complete n H)
| false => fun _ => None
end eq_refl.
But the idea is the same. By instantiating eq_refl outside the pattern matching, you do not lose any information when matching on is_1 n.