diff options
Diffstat (limited to 'theories/Program/Subset.v')
-rw-r--r-- | theories/Program/Subset.v | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v new file mode 100644 index 00000000..d021326a --- /dev/null +++ b/theories/Program/Subset.v @@ -0,0 +1,116 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Coq.Program.Utils. +Require Import Coq.Program.Equality. + +Open Local Scope program_scope. + +(** 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. +Proof. + induction n. + induction m. + simpl. + split ; intros ; subst. + + inversion H. + reflexivity. + + pi. +Qed. + +(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] + in tactics. *) + +Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B := + fn (exist _ x (refl_equal x)). + +(* This is what we want to be able to do: replace the originaly matched object by a new, + propositionally equal one. If [fn] works on [x] it should work on any [y | y = 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. +Proof. + intros. + unfold match_eq. + f_equal. + destruct y. + (* uses proof-irrelevance *) + apply <- subset_eq. + symmetry. assumption. +Qed. + +(** 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]. *) + +Ltac rewrite_match_eq H := + match goal with + [ |- ?T ] => + match T with + context [ match_eq ?A ?B ?t ?f ] => + rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H))) + end + end. + +(** Otherwise we can simply unfold [match_eq] and the term trivially reduces to the original definition. *) + +Ltac simpl_match_eq := unfold match_eq ; simpl. |