Library Coq.Program.Subset
Tactics related to subsets and proof irrelevance.
The following tactics implement a poor-man's solution for proof-irrelevance: it tries to
factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial.
Ltac on_subset_proof_aux tac T :=
match T with
|
context [
exist ?
P _ ?
p ] =>
try on_subset_proof_aux tac P ;
tac p
end.
Ltac on_subset_proof tac :=
match goal with
[ |- ?
T ] =>
on_subset_proof_aux tac T
end.
Ltac abstract_any_hyp H´ p :=
match type of p with
?
X =>
match goal with
| [
H :
X |-
_ ] =>
fail 1
|
_ =>
set (
H´:=
p) ;
try (
change p with H´) ;
clearbody H´
end
end.
Ltac abstract_subset_proof :=
on_subset_proof ltac:(
fun p =>
let H :=
fresh "eqH"
in abstract_any_hyp H p ;
simpl in H).
Ltac abstract_subset_proofs :=
repeat abstract_subset_proof.
Ltac pi_subset_proof_hyp p :=
match type of p with
?
X =>
match goal with
| [
H :
X |-
_ ] =>
match p with
|
H =>
fail 2
|
_ =>
rewrite (
proof_irrelevance X p H)
end
|
_ =>
fail " No hypothesis with same type "
end
end.
Ltac pi_subset_proof :=
on_subset_proof pi_subset_proof_hyp.
Ltac pi_subset_proofs :=
repeat pi_subset_proof.
The two preceding tactics in sequence.
Now we make a tactic to be able to rewrite a term t which is applied to a match_eq using an arbitrary
equality t = u, and u is now the subject of the match.
Otherwise we can simply unfold match_eq and the term trivially reduces to the original definition.
Ltac simpl_match_eq :=
unfold match_eq ;
simpl.