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.
Ltac clear_subset_proofs :=
abstract_subset_proofs ;
simpl in * |- ;
pi_subset_proofs ;
clear_dups.
Ltac pi :=
repeat progress f_equal ;
apply proof_irrelevance.
Lemma subset_eq :
forall A (
P :
A ->
Prop) (
n m :
sig P),
n =
m <-> `
n = `
m.
Definition match_eq (
A B :
Type) (
x :
A) (
fn :
forall (
y :
A |
y =
x),
B) :
B :=
fn (
exist _ x (
refl_equal x)).
Lemma match_eq_rewrite :
forall (
A B :
Type) (
x :
A) (
fn :
forall (
y :
A |
y =
x),
B)
(
y :
A |
y =
x),
match_eq A B x fn =
fn y.
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.