diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 57 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 71 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 264 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 109 | ||||
| -rw-r--r-- | theories/Program/Program.v | 7 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 116 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 59 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 234 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 56 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 148 |
10 files changed, 1121 insertions, 0 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v new file mode 100644 index 00000000..a1a78acc --- /dev/null +++ b/theories/Program/Basics.v @@ -0,0 +1,57 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Standard functions and combinators. + * Proofs about them require functional extensionality and can be found in [Combinators]. + * + * Author: Matthieu Sozeau + * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + * 91405 Orsay, France *) + +(* $Id: Basics.v 11046 2008-06-03 22:48:06Z msozeau $ *) + +(** The polymorphic identity function. *) + +Definition id {A} := fun x : A => x. + +(** Function composition. *) + +Definition compose {A B C} (g : B -> C) (f : A -> B) := + fun x : A => g (f x). + +Hint Unfold compose. + +Notation " g ∘ f " := (compose g f) + (at level 40, left associativity) : program_scope. + +Open Local Scope program_scope. + +(** The non-dependent function space between [A] and [B]. *) + +Definition arrow (A B : Type) := A -> B. + +(** Logical implication. *) + +Definition impl (A B : Prop) : Prop := A -> B. + +(** The constant function [const a] always returns [a]. *) + +Definition const {A B} (a : A) := fun _ : B => a. + +(** The [flip] combinator reverses the first two arguments of a function. *) + +Definition flip {A B C} (f : A -> B -> C) x y := f y x. + +(** Application as a combinator. *) + +Definition apply {A B} (f : A -> B) (x : A) := f x. + +(** Curryfication of [prod] is defined in [Logic.Datatypes]. *) + +Implicit Arguments prod_curry [[A] [B] [C]]. +Implicit Arguments prod_uncurry [[A] [B] [C]]. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v new file mode 100644 index 00000000..e267fbbe --- /dev/null +++ b/theories/Program/Combinators.v @@ -0,0 +1,71 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Proofs about standard combinators, exports functional extensionality. + * + * Author: Matthieu Sozeau + * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + * 91405 Orsay, France *) + +Require Import Coq.Program.Basics. +Require Export Coq.Program.FunctionalExtensionality. + +Open Scope program_scope. + +(** Composition has [id] for neutral element and is associative. *) + +Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. +Proof. + intros. + unfold id, compose. + symmetry. apply eta_expansion. +Qed. + +Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. +Proof. + intros. + unfold id, compose. + symmetry ; apply eta_expansion. +Qed. + +Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), + h ∘ g ∘ f = h ∘ (g ∘ f). +Proof. + intros. + reflexivity. +Qed. + +Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. + +(** [flip] is involutive. *) + +Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id. +Proof. + unfold flip, compose. + intros. + extensionality x ; extensionality y ; extensionality z. + reflexivity. +Qed. + +(** [prod_curry] and [prod_uncurry] are each others inverses. *) + +Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id. +Proof. + simpl ; intros. + unfold prod_uncurry, prod_curry, compose. + extensionality x ; extensionality y ; extensionality z. + reflexivity. +Qed. + +Lemma prod_curry_uncurry : forall A B C, @prod_curry A B C ∘ prod_uncurry = id. +Proof. + simpl ; intros. + unfold prod_uncurry, prod_curry, compose. + extensionality x ; extensionality p. + destruct p ; simpl ; reflexivity. +Qed. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v new file mode 100644 index 00000000..d19f29c3 --- /dev/null +++ b/theories/Program/Equality.v @@ -0,0 +1,264 @@ +(* -*- coq-prog-args: ("-emacs-U") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Equality.v 11023 2008-05-30 11:08:39Z msozeau $ i*) + +(** Tactics related to (dependent) equality and proof irrelevance. *) + +Require Export ProofIrrelevance. +Require Export JMeq. + +Require Import Coq.Program.Tactics. + +(** Notation for heterogenous equality. *) + +Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). + +(** Do something on an heterogeneous equality appearing in the context. *) + +Ltac on_JMeq tac := + match goal with + | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H + end. + +(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) + +Ltac simpl_one_JMeq := + on_JMeq ltac:(fun H => replace_hyp H (JMeq_eq H)). + +(** Repeat it for every possible hypothesis. *) + +Ltac simpl_JMeq := repeat simpl_one_JMeq. + +(** Just simplify an h.eq. without clearing it. *) + +Ltac simpl_one_dep_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H)). + +Require Import Eqdep. + +(** Simplify dependent equality using sigmas to equality of the second projections if possible. + Uses UIP. *) + +Ltac simpl_existT := + match goal with + [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => + let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H + end. + +Ltac simpl_existTs := repeat simpl_existT. + +(** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *) + +Ltac elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + end + end. + +(** Rewrite using uniqueness of indentity proofs [H = refl_equal X]. *) + +Ltac simpl_uip := + match goal with + [ H : ?X = ?X |- _ ] => rewrite (UIP_refl _ _ H) in *; clear H + end. + +(** Simplify equalities appearing in the context and goal. *) + +Ltac simpl_eq := simpl ; repeat (elim_eq_rect ; simpl) ; repeat (simpl_uip ; simpl). + +(** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *) + +Ltac abstract_eq_hyp H' p := + let ty := type of p in + let tyred := eval simpl in ty in + match tyred with + ?X = ?Y => + match goal with + | [ H : X = Y |- _ ] => fail 1 + | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H' + end + end. + +(** Apply the tactic tac to proofs of equality appearing as coercion arguments. + Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators. + *) + +Ltac on_coerce_proof tac T := + match T with + | context [ eq_rect _ _ _ _ ?p ] => tac p + end. + +Ltac on_coerce_proof_gl tac := + match goal with + [ |- ?T ] => on_coerce_proof tac T + end. + +(** Abstract proofs of equalities of coercions. *) + +Ltac abstract_eq_proof := on_coerce_proof_gl ltac:(fun p => let H := fresh "eqH" in abstract_eq_hyp H p). + +Ltac abstract_eq_proofs := repeat abstract_eq_proof. + +(** Factorize proofs, by using proof irrelevance so that two proofs of the same equality + in the goal become convertible. *) + +Ltac pi_eq_proof_hyp p := + let ty := type of p in + let tyred := eval simpl in ty in + match tyred with + ?X = ?Y => + match goal with + | [ H : X = Y |- _ ] => + match p with + | H => fail 2 + | _ => rewrite (proof_irrelevance (X = Y) p H) + end + | _ => fail " No hypothesis with same type " + end + end. + +(** Factorize proofs of equality appearing as coercion arguments. *) + +Ltac pi_eq_proof := on_coerce_proof_gl pi_eq_proof_hyp. + +Ltac pi_eq_proofs := repeat pi_eq_proof. + +(** The two preceding tactics in sequence. *) + +Ltac clear_eq_proofs := + abstract_eq_proofs ; pi_eq_proofs. + +Hint Rewrite <- eq_rect_eq : refl_id. + +(** The refl_id database should be populated with lemmas of the form + [coerce_* t (refl_equal _) = t]. *) + +Ltac rewrite_refl_id := autorewrite with refl_id. + +(** Clear the context and goal of equality proofs. *) + +Ltac clear_eq_ctx := + rewrite_refl_id ; clear_eq_proofs. + +(** Reapeated elimination of [eq_rect] applications. + Abstracting equalities makes it run much faster than an naive implementation. *) + +Ltac simpl_eqs := + repeat (elim_eq_rect ; simpl ; clear_eq_ctx). + +(** Clear unused reflexivity proofs. *) + +Ltac clear_refl_eq := + match goal with [ H : ?X = ?X |- _ ] => clear H end. +Ltac clear_refl_eqs := repeat clear_refl_eq. + +(** Clear unused equality proofs. *) + +Ltac clear_eq := + match goal with [ H : _ = _ |- _ ] => clear H end. +Ltac clear_eqs := repeat clear_eq. + +(** Combine all the tactics to simplify goals containing coercions. *) + +Ltac simplify_eqs := + simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ; + try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id. + +(** A tactic that tries to remove trivial equality guards in induction hypotheses coming + from [dependent induction]/[generalize_eqs] invocations. *) + + +Ltac simpl_IH_eq H := + match type of H with + | @JMeq _ ?x _ _ -> _ => + refine_hyp (H (JMeq_refl x)) + | _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ (JMeq_refl x)) + | _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ (JMeq_refl x)) + | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ _ (JMeq_refl x)) + | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ _ _ (JMeq_refl x)) + | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ _ _ _ (JMeq_refl x)) + | ?x = _ -> _ => + refine_hyp (H (refl_equal x)) + | _ -> ?x = _ -> _ => + refine_hyp (H _ (refl_equal x)) + | _ -> _ -> ?x = _ -> _ => + refine_hyp (H _ _ (refl_equal x)) + | _ -> _ -> _ -> ?x = _ -> _ => + refine_hyp (H _ _ _ (refl_equal x)) + | _ -> _ -> _ -> _ -> ?x = _ -> _ => + refine_hyp (H _ _ _ _ (refl_equal x)) + | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ => + refine_hyp (H _ _ _ _ _ (refl_equal x)) + end. + +Ltac simpl_IH_eqs H := repeat simpl_IH_eq H. + +Ltac do_simpl_IHs_eqs := + match goal with + | [ H : context [ @JMeq _ _ _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) + | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) + end. + +Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs. + +Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; + simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs. + +(** The following tactics allow to do induction on an already instantiated inductive predicate + by first generalizing it and adding the proper equalities to the context, in a maner similar to + the BasicElim tactic of "Elimination with a motive" by Conor McBride. *) + +(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis + and starts a dependent induction using this tactic. *) + +Ltac do_depind tac H := + generalize_eqs H ; tac H ; repeat progress simpl_depind. + +(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *) + +Tactic Notation "dependent" "destruction" ident(H) := + do_depind ltac:(fun H => destruct H ; intros) H ; subst*. + +Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := + do_depind ltac:(fun H => destruct H using c ; intros) H. + +(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by + writting another wrapper calling do_depind. *) + +Tactic Notation "dependent" "induction" ident(H) := + do_depind ltac:(fun H => induction H ; intros) H. + +Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := + do_depind ltac:(fun H => induction H using c ; intros) H. + +(** This tactic also generalizes the goal by the given variables before the induction. *) + +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := + do_depind ltac:(fun H => generalize l ; clear l ; induction H ; intros) H. + +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := + do_depind ltac:(fun H => generalize l ; clear l ; induction H using c ; intros) H. + diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v new file mode 100644 index 00000000..b5ad5b4d --- /dev/null +++ b/theories/Program/FunctionalExtensionality.v @@ -0,0 +1,109 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: FunctionalExtensionality.v 10739 2008-04-01 14:45:20Z herbelin $ i*) + +(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. + It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. + + It also defines two lemmas for expansion of fixpoint defs using extensionnality and proof-irrelevance + to avoid a side condition on the functionals. *) + +Require Import Coq.Program.Utils. +Require Import Coq.Program.Wf. +Require Import Coq.Program.Equality. + +Set Implicit Arguments. +Unset Strict Implicit. + +(** The converse of functional equality. *) + +Lemma equal_f : forall A B : Type, forall (f g : A -> B), + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + +(** Statements of functional equality for simple and dependent functions. *) + +Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), + forall (f g : forall x : A, B x), + (forall x, f x = g x) -> f = g. + +Lemma fun_extensionality : forall A B (f g : A -> B), + (forall x, f x = g x) -> f = g. +Proof. + intros ; apply fun_extensionality_dep. + assumption. +Qed. + +Hint Resolve fun_extensionality fun_extensionality_dep : program. + +(** Apply [fun_extensionality], introducing variable x. *) + +Tactic Notation "extensionality" ident(x) := + match goal with + [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x + end. + +(** Eta expansion follows from extensionality. *) + +Lemma eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), + f = fun x => f x. +Proof. + intros. + extensionality x. + reflexivity. +Qed. + +Lemma eta_expansion : forall A B (f : A -> B), + f = fun x => f x. +Proof. + intros ; apply eta_expansion_dep. +Qed. + +(** The two following lemmas allow to unfold a well-founded fixpoint definition without + restriction using the functional extensionality axiom. *) + +(** For a function defined with Program using a well-founded order. *) + +Program Lemma fix_sub_eq_ext : + forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Set) + (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), + forall x : A, + Fix_sub A R Rwf P F_sub x = + F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y). +Proof. + intros ; apply Fix_eq ; auto. + intros. + assert(f = g). + extensionality y ; apply H. + rewrite H0 ; auto. +Qed. + +(** For a function defined with Program using a measure. *) + +Program Lemma fix_sub_measure_eq_ext : + forall (A : Type) (f : A -> nat) (P : A -> Type) + (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x), + forall x : A, + Fix_measure_sub A f P F_sub x = + F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y). +Proof. + intros ; apply Fix_measure_eq ; auto. + intros. + assert(f0 = g). + extensionality y ; apply H. + rewrite H0 ; auto. +Qed. + + diff --git a/theories/Program/Program.v b/theories/Program/Program.v new file mode 100644 index 00000000..b6c3031e --- /dev/null +++ b/theories/Program/Program.v @@ -0,0 +1,7 @@ +Require Export Coq.Program.Utils. +Require Export Coq.Program.Wf. +Require Export Coq.Program.Equality. +Require Export Coq.Program.Subset. +Require Export Coq.Program.Basics. +Require Export Coq.Program.Combinators. +Require Export Coq.Program.Syntax.
\ No newline at end of file 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. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v new file mode 100644 index 00000000..6cd75257 --- /dev/null +++ b/theories/Program/Syntax.v @@ -0,0 +1,59 @@ +(* -*- coq-prog-args: ("-emacs-U") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Custom notations and implicits for Coq prelude definitions. + * + * Author: Matthieu Sozeau + * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + * 91405 Orsay, France *) + +(** Notations for the unit type and value. *) + +Notation " () " := Datatypes.unit : type_scope. +Notation " () " := tt. + +(** Set maximally inserted implicit arguments for standard definitions. *) + +Implicit Arguments eq [[A]]. + +Implicit Arguments Some [[A]]. +Implicit Arguments None [[A]]. + +Implicit Arguments inl [[A] [B]]. +Implicit Arguments inr [[A] [B]]. + +Implicit Arguments left [[A] [B]]. +Implicit Arguments right [[A] [B]]. + +Require Import Coq.Lists.List. + +Implicit Arguments nil [[A]]. +Implicit Arguments cons [[A]]. + +(** Standard notations for lists. *) + +Notation " [ ] " := nil : list_scope. +Notation " [ x ] " := (cons x nil) : list_scope. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. + +(** n-ary exists *) + +Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) + (at level 200, x ident, y ident, right associativity) : type_scope. + +Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))))) + (at level 200, x ident, y ident, z ident, right associativity) : type_scope. + +Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p)))))))) + (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope. + +Tactic Notation "exist" constr(x) := exists x. +Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. +Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. +Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v new file mode 100644 index 00000000..41b170c9 --- /dev/null +++ b/theories/Program/Tactics.v @@ -0,0 +1,234 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Tactics.v 11122 2008-06-13 14:18:44Z msozeau $ i*) + +(** This module implements various tactics used to simplify the goals produced by Program, + which are also generally useful. *) + +(** Destructs one pair, without care regarding naming. *) + +Ltac destruct_one_pair := + match goal with + | [H : (_ /\ _) |- _] => destruct H + | [H : prod _ _ |- _] => destruct H + end. + +(** Repeateadly destruct pairs. *) + +Ltac destruct_pairs := repeat (destruct_one_pair). + +(** Destruct one existential package, keeping the name of the hypothesis for the first component. *) + +Ltac destruct_one_ex := + let tac H := let ph := fresh "H" in (destruct H as [H ph]) in + let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in + match goal with + | [H : (ex _) |- _] => tac H + | [H : (sig ?P) |- _ ] => tac H + | [H : (sigT ?P) |- _ ] => tacT H + | [H : (ex2 _) |- _] => tac H + end. + +(** Repeateadly destruct existentials. *) + +Ltac destruct_exists := repeat (destruct_one_ex). + +(** Repeateadly destruct conjunctions and existentials. *) + +Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). + +(** Destruct an existential hypothesis [t] keeping its name for the first component + and using [Ht] for the second *) + +Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. + +(** Destruct a disjunction keeping its name in both subgoals. *) + +Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. + +(** Discriminate that also work on a [x <> x] hypothesis. *) + +Ltac discriminates := + match goal with + | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity + | _ => discriminate + end. + +(** Revert the last hypothesis. *) + +Ltac revert_last := + match goal with + [ H : _ |- _ ] => revert H + end. + +(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *) + +Ltac reverse := repeat revert_last. + +(** Clear duplicated hypotheses *) + +Ltac clear_dup := + match goal with + | [ H : ?X |- _ ] => + match goal with + | [ H' : X |- _ ] => + match H' with + | H => fail 2 + | _ => clear H' || clear H + end + end + end. + +Ltac clear_dups := repeat clear_dup. + +(** A non-failing subst that substitutes as much as possible. *) + +Ltac subst_no_fail := + repeat (match goal with + [ H : ?X = ?Y |- _ ] => subst X || subst Y + end). + +Tactic Notation "subst" "*" := subst_no_fail. + +Ltac on_application f tac T := + match T with + | context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c) + | context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b) + | context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a) + | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) + | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) + | context [f ?x ?y ?z ?w] => tac (f x y z w) + | context [f ?x ?y ?z] => tac (f x y z) + | context [f ?x ?y] => tac (f x y) + | context [f ?x] => tac (f x) + end. + +(** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) + +Ltac on_call f tac := + match goal with + | |- ?T => on_application f tac T + | H : ?T |- _ => on_application f tac T + end. + +(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object. *) + +Ltac destruct_call f := + let tac t := (destruct t) in on_call f tac. + +Ltac destruct_calls f := repeat destruct_call f. + +Ltac destruct_call_in f H := + let tac t := (destruct t) in + let T := type of H in + on_application f tac T. + +Ltac destruct_call_as f l := + let tac t := (destruct t as l) in on_call f tac. + +Ltac destruct_call_as_in f l H := + let tac t := (destruct t as l) in + let T := type of H in + on_application f tac T. + +Tactic Notation "destruct_call" constr(f) := destruct_call f. + +(** Permit to name the results of destructing the call to [f]. *) + +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := + destruct_call_as f l. + +(** Specify the hypothesis in which the call occurs as well. *) + +Tactic Notation "destruct_call" constr(f) "in" hyp(id) := + destruct_call_in f id. + +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := + destruct_call_as_in f l id. + +(** Try to inject any potential constructor equality hypothesis. *) + +Ltac autoinjection := + let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in + match goal with + | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H + | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H + | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H + end. + +Ltac autoinjections := repeat autoinjection. + +(** Destruct an hypothesis by first copying it to avoid dependencies. *) + +Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. + +(** If bang appears in the goal, it means that we have a proof of False and the goal is solved. *) + +Ltac bang := + match goal with + | |- ?x => + match x with + | context [False_rect _ ?p] => elim p + end + end. + +(** A tactic to show contradiction by first asserting an automatically provable hypothesis. *) +Tactic Notation "contradiction" "by" constr(t) := + let H := fresh in assert t as H by auto with * ; contradiction. + +(** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal. + Useful to do saturation using tactics. *) + +Ltac add_hypothesis 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. + +(** A tactic to replace an hypothesis by another term. *) + +Ltac replace_hyp H c := + let H' := fresh "H" in + assert(H' := c) ; clear H ; rename H' into H. + +(** A tactic to refine an hypothesis by supplying some of its arguments. *) + +Ltac refine_hyp c := + let tac H := replace_hyp H c in + match c with + | ?H _ => tac H + | ?H _ _ => tac H + | ?H _ _ _ => tac H + | ?H _ _ _ _ => tac H + | ?H _ _ _ _ _ => tac H + | ?H _ _ _ _ _ _ => tac H + | ?H _ _ _ _ _ _ _ => tac H + | ?H _ _ _ _ _ _ _ _ => tac H + end. + +(** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto] + is not enough, better rebind using [Obligations Tactic := tac] in this case, + possibly using [program_simplify] to use standard goal-cleaning tactics. *) + +Ltac program_simplify := + simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; autoinjections ; try discriminates ; + try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). + +Ltac program_simpl := program_simplify ; auto. + +Ltac obligations_tactic := program_simpl. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v new file mode 100644 index 00000000..21eee0ca --- /dev/null +++ b/theories/Program/Utils.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Utils.v 10919 2008-05-11 22:04:26Z msozeau $ i*) + +Require Export Coq.Program.Tactics. + +Set Implicit Arguments. + +(** A simpler notation for subsets defined on a cartesian product. *) + +Notation "{ ( x , y ) : A | P }" := + (sig (fun anonymous : A => let (x,y) := anonymous in P)) + (x ident, y ident, at level 10) : type_scope. + +(** Generates an obligation to prove False. *) + +Notation " ! " := (False_rect _ _) : program_scope. + +Delimit Scope program_scope with prg. + +(** Abbreviation for first projection and hiding of proofs of subset objects. *) + +Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. + +(** Coerces objects to their support before comparing them. *) + +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope. + +Require Import Coq.Bool.Sumbool. + +(** Construct a dependent disjunction from a boolean. *) + +Notation dec := sumbool_of_bool. + +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) + +(** Hide proofs and generates obligations when put in a term. *) + +Notation "'in_left'" := (@left _ _ _) : program_scope. +Notation "'in_right'" := (@right _ _ _) : program_scope. + +(** Extraction directives *) +(* +Extraction Inline proj1_sig. +Extract Inductive unit => "unit" [ "()" ]. +Extract Inductive bool => "bool" [ "true" "false" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. +(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) +(* Extract Inductive sigT => "prod" [ "" ]. *) +*)
\ No newline at end of file diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v new file mode 100644 index 00000000..b6ba5d44 --- /dev/null +++ b/theories/Program/Wf.v @@ -0,0 +1,148 @@ +Require Import Coq.Init.Wf. +Require Import Coq.Program.Utils. +Require Import ProofIrrelevance. + +Open Local Scope program_scope. + +Implicit Arguments Acc_inv [A R x y]. + +(** Reformulation of the Wellfounded module using subsets where possible. *) + +Section Well_founded. + Variable A : Type. + Variable R : A -> A -> Prop. + Hypothesis Rwf : well_founded R. + + Section Acc. + + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. + + Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := + F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) + (Acc_inv r (proj2_sig y))). + + Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + End Acc. + + Section FixPoint. + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. + + Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) + + Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). + + Hypothesis + F_ext : + forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), + (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. + + Lemma Fix_F_eq : + forall (x:A) (r:Acc R x), + F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. + + Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s. + Proof. + intro x; induction (Rwf x); intros. + rewrite (proof_irrelevance (Acc R x) r s) ; auto. + Qed. + + Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)). + Proof. + intro x; unfold Fix in |- *. + rewrite <- (Fix_F_eq ). + apply F_ext; intros. + apply Fix_F_inv. + Qed. + + Lemma fix_sub_eq : + forall x : A, + Fix_sub P F_sub x = + let f_sub := F_sub in + f_sub x (fun (y : A | R y x) => Fix (`y)). + exact Fix_eq. + Qed. + + End FixPoint. + +End Well_founded. + +Extraction Inline Fix_F_sub Fix_sub. + +Require Import Wf_nat. +Require Import Lt. + +Section Well_founded_measure. + Variable A : Type. + Variable m : A -> nat. + + Section Acc. + + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. + + Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := + F_sub x (fun (y : A | m y < m x) => Fix_measure_F_sub y + (@Acc_inv _ _ _ r (m y) (proj2_sig y))). + + Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). + + End Acc. + + Section FixPoint. + Variable P : A -> Type. + + Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x. + + Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) + + Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)). + + Hypothesis + F_ext : + forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)), + (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. + + Program Lemma Fix_measure_F_eq : + forall (x:A) (r:Acc lt (m x)), + F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r. + Proof. + intros x. + set (y := m x). + unfold Fix_measure_F_sub. + intros r ; case r ; auto. + Qed. + + Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s. + Proof. + intros x r s. + rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto. + Qed. + + Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)). + Proof. + intro x; unfold Fix_measure in |- *. + rewrite <- (Fix_measure_F_eq ). + apply F_ext; intros. + apply Fix_measure_F_inv. + Qed. + + Lemma fix_measure_sub_eq : forall x : A, + Fix_measure_sub P F_sub x = + let f_sub := F_sub in + f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)). + exact Fix_measure_eq. + Qed. + + End FixPoint. + +End Well_founded_measure. + +Extraction Inline Fix_measure_F_sub Fix_measure_sub. |