From 2de683db51b44b8051ead6d89be67f0185e7e87d Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 7 Aug 2007 18:36:25 +0000 Subject: Move Program tactics into a proper theories/ directory as they are general purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 6 +- contrib/subtac/FixSub.v | 147 ------------------------- contrib/subtac/FunctionalExtensionality.v | 47 -------- contrib/subtac/Heq.v | 34 ------ contrib/subtac/Subtac.v | 2 - contrib/subtac/SubtacTactics.v | 158 -------------------------- contrib/subtac/Utils.v | 65 ----------- contrib/subtac/subtac.ml | 8 +- contrib/subtac/subtac_obligations.ml | 4 +- contrib/subtac/subtac_utils.ml | 18 +-- contrib/subtac/subtac_utils.mli | 2 +- doc/refman/RefMan-ind.tex | 2 +- theories/Init/Prelude.v | 2 +- theories/Program/FixSub.v | 148 +++++++++++++++++++++++++ theories/Program/FunctionalExtensionality.v | 65 +++++++++++ theories/Program/Heq.v | 63 +++++++++++ theories/Program/Program.v | 3 + theories/Program/Tactics.v | 165 ++++++++++++++++++++++++++++ theories/Program/Utils.v | 70 ++++++++++++ 19 files changed, 537 insertions(+), 472 deletions(-) delete mode 100644 contrib/subtac/FixSub.v delete mode 100644 contrib/subtac/FunctionalExtensionality.v delete mode 100644 contrib/subtac/Heq.v delete mode 100644 contrib/subtac/Subtac.v delete mode 100644 contrib/subtac/SubtacTactics.v delete mode 100644 contrib/subtac/Utils.v create mode 100644 theories/Program/FixSub.v create mode 100644 theories/Program/FunctionalExtensionality.v create mode 100644 theories/Program/Heq.v create mode 100644 theories/Program/Program.v create mode 100644 theories/Program/Tactics.v create mode 100644 theories/Program/Utils.v diff --git a/Makefile.common b/Makefile.common index cd0d6ab790..1325eabcf1 100644 --- a/Makefile.common +++ b/Makefile.common @@ -751,9 +751,9 @@ CCVO:= DPVO:=contrib/dp/Dp.vo -SUBTACVO:=contrib/subtac/SubtacTactics.vo contrib/subtac/Heq.vo \ - contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ - contrib/subtac/FunctionalExtensionality.vo +SUBTACVO:=theories/Program/Tactics.vo theories/Program/Heq.vo \ + theories/Program/Utils.vo theories/Program/FixSub.vo theories/Program/Program.vo \ + theories/Program/FunctionalExtensionality.vo RTAUTOVO:= \ contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v deleted file mode 100644 index f047b729dd..0000000000 --- a/contrib/subtac/FixSub.v +++ /dev/null @@ -1,147 +0,0 @@ -Require Import Wf. -Require Import Coq.subtac.Utils. - -(** 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 (proj1_sig y) (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:{ 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:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (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 <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros. - apply F_ext; auto. - intros. - rewrite (proof_irrelevance (Acc R x) r s) ; auto. - Qed. - - Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{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. - - Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := - F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) - (Acc_inv r (m (proj1_sig 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. - - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig 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. - - Lemma Fix_measure_F_eq : - forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (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. diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v deleted file mode 100644 index 4610f3467a..0000000000 --- a/contrib/subtac/FunctionalExtensionality.v +++ /dev/null @@ -1,47 +0,0 @@ -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. - -Axiom fun_extensionality : forall A B (f g : A -> B), - (forall x, f x = g x) -> f = g. - -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. - -Hint Resolve fun_extensionality fun_extensionality_dep : subtac. - -Require Import Coq.subtac.Utils. -Require Import Coq.subtac.FixSub. - -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). - apply (fun_extensionality_dep _ _ _ _ H). - rewrite H0 ; auto. -Qed. - -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). - apply (fun_extensionality_dep _ _ _ _ H). - rewrite H0 ; auto. -Qed. diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v deleted file mode 100644 index f2b216d960..0000000000 --- a/contrib/subtac/Heq.v +++ /dev/null @@ -1,34 +0,0 @@ -Require Export JMeq. - -(** 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 => let H' := fresh "H" in - assert (H' := JMeq_eq H) ; clear H ; rename H' into 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)). - - - - diff --git a/contrib/subtac/Subtac.v b/contrib/subtac/Subtac.v deleted file mode 100644 index 9912cd242c..0000000000 --- a/contrib/subtac/Subtac.v +++ /dev/null @@ -1,2 +0,0 @@ -Require Export Coq.subtac.Utils. -Require Export Coq.subtac.FixSub. \ No newline at end of file diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v deleted file mode 100644 index a00234dde8..0000000000 --- a/contrib/subtac/SubtacTactics.v +++ /dev/null @@ -1,158 +0,0 @@ -Ltac induction_with_subterm c H := - let x := fresh "x" in - let y := fresh "y" in - (remember c as x ; rewrite <- y in H ; induction H ; subst). - -Ltac induction_on_subterm c := - let x := fresh "x" in - let y := fresh "y" in - (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; - clear y). - -Ltac induction_with_subterms c c' H := - let x := fresh "x" in - let y := fresh "y" in - let z := fresh "z" in - let w := fresh "w" in - (set(x := c) ; assert(y:x = c) by reflexivity ; - set(z := c') ; assert(w:z = c') by reflexivity ; - rewrite <- y in H ; rewrite <- w in H ; - induction H ; subst). - - -Ltac destruct_one_pair := - match goal with - | [H : (_ /\ _) |- _] => destruct H - | [H : prod _ _ |- _] => destruct H - end. - -Ltac destruct_pairs := repeat (destruct_one_pair). - -Ltac destruct_one_ex := - let tac H := let ph := fresh "H" in destruct H as [H ph] in - match goal with - | [H : (ex _) |- _] => tac H - | [H : (sig ?P) |- _ ] => tac H - | [H : (ex2 _) |- _] => tac H - end. - -Ltac destruct_exists := repeat (destruct_one_ex). - -Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. - -Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. - -Tactic Notation "contradiction" "by" constr(t) := - let H := fresh in assert t as H by auto with * ; contradiction. - -Ltac discriminates := - match goal with - | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity - | _ => discriminate - end. - -Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). - -Ltac on_last_hyp tac := - match goal with - [ H : _ |- _ ] => tac H - end. - -Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t. - -Ltac revert_last := - match goal with - [ H : _ |- _ ] => revert H - end. - -Ltac reverse := repeat revert_last. - -Ltac on_call f tac := - match goal with - | H : ?T |- _ => - match T with - | 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 - | |- ?T => - match T with - | 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 - 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_call_as f l := - let tac t := destruct t as l in on_call f tac. - -Tactic Notation "destruct_call" constr(f) := destruct_call f. -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. - -Ltac myinjection := - let tac H := inversion H ; subst ; 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 - | _ => idtac - end. - -Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. - -Ltac bang := - match goal with - | |- ?x => - match x with - | context [False_rect _ ?p] => elim p - end - end. - -Require Import Eqdep. - -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 ; - try ((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 ; - try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - end - end. - -Ltac real_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. - \ No newline at end of file diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v deleted file mode 100644 index 76f49dd3bc..0000000000 --- a/contrib/subtac/Utils.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Export Coq.subtac.SubtacTactics. - -Set Implicit Arguments. - -(** Wrap a proposition inside a subset. *) - -Notation " {{ x }} " := (tt : { y : unit | x }). - -(** 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) : type_scope. - -(** Generates an obligation to prove False. *) - -Notation " ! " := (False_rect _ _). - -(** Abbreviation for first projection and hiding of proofs of subset objects. *) - -Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. - -(** Coerces objects to their support before comparing them. *) - -Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). - -(** Quantifying over subsets. *) - -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). - -Notation "'forall' { x : A | P } , Q" := - (forall x:{x:A|P}, Q) - (at level 200, x ident, right associativity). - -Require Import Coq.Bool.Sumbool. - -(** Construct a dependent disjunction from a boolean. *) - -Notation "'dec'" := (sumbool_of_bool) (at level 0). - -(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) - -Notation in_right := (@right _ _ _). -Notation in_left := (@left _ _ _). - -(** Default simplification tactic. *) - -Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; - try (solve [ red ; intros ; discriminate ]) ; auto with *. - -(** 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" [ "" ]. *) - -Require Export ProofIrrelevance. -Require Export Coq.subtac.Heq. - -Delimit Scope program_scope with program. diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index e774dd127a..d38bdb79ef 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -95,8 +95,8 @@ let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; (* check_required_library ["Coq";"Logic";"JMeq"]; *) - require_library "Coq.subtac.FixSub"; - require_library "Coq.subtac.Utils"; + require_library "Coq.Program.FixSub"; + require_library "Coq.Program.Tactics"; require_library "Coq.Logic.JMeq"; let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in @@ -125,6 +125,10 @@ let subtac (loc, command) = | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl +(* | VernacCoFixpoint (l, b) -> *) +(* let _ = trace (str "Building cofixpoint") in *) +(* ignore(Subtac_command.build_recursive l b) *) + (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 1bd85b92bd..656c4397d3 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -13,7 +13,7 @@ open Decl_kinds open Util open Evd -let pperror cmd = Util.errorlabstrm "Subtac" cmd +let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) exception NoObligations of identifier option @@ -96,7 +96,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty let freeze () = !from_prg, !default_tactic_expr let unfreeze (v, t) = from_prg := v; set_default_tactic t let init () = - from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" []) + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "program_simpl" []) let _ = Summary.declare_summary "program-tcc-table" diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index b557b40569..e5ac65878d 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -10,7 +10,7 @@ let ($) f x = f x (****************************************************************************) (* Library linking *) -let contrib_name = "subtac" +let contrib_name = "Program" let subtac_dir = [contrib_name] let fix_sub_module = "FixSub" @@ -28,8 +28,8 @@ let make_ref l s = lazy (init_reference l s) let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded" let acc_ref = make_ref ["Init";"Wf"] "Acc" let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv" -let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub" -let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub" +let fix_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_sub" +let fix_measure_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_measure_sub" let lt_ref = make_ref ["Init";"Peano"] "lt" let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf" let refl_ref = make_ref ["Init";"Logic"] "refl_equal" @@ -441,11 +441,11 @@ let pr_evar_defs evd = str"METAS:"++brk(0,1)++pr_meta_map evd in v 0 (pp_evm ++ pp_met) -let subtac_utils_path = - make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"]) -let utils_tac s = - lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s)) +let contrib_tactics_path = + make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"]) +let tactics_tac s = + lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) -let utils_call tac args = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args)) +let tactics_call tac args = + TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 5a5dd4274b..bbf536c41f 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -125,6 +125,6 @@ val string_of_intset : Intset.t -> string val pr_evar_defs : evar_defs -> Pp.std_ppcmds -val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr +val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex index 0d5017f8ba..ecb872b0e8 100644 --- a/doc/refman/RefMan-ind.tex +++ b/doc/refman/RefMan-ind.tex @@ -502,7 +502,7 @@ conjunction of their conclusions. For exemple, we can combine the induction principles for trees and forests: \begin{coq_example*} -Mutual Scheme tree_forest_mutind from tree_ind, forest_ind. +Combined Scheme tree_forest_mutind from tree_ind, forest_ind. Check tree_forest_mutind. \end{coq_example*} diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6022da116c..1915ad37cb 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -14,4 +14,4 @@ Require Export Datatypes. Require Export Specif. Require Export Peano. Require Export Wf. -Require Export Tactics. +Require Export Coq.Init.Tactics. diff --git a/theories/Program/FixSub.v b/theories/Program/FixSub.v new file mode 100644 index 0000000000..58ac9d90ee --- /dev/null +++ b/theories/Program/FixSub.v @@ -0,0 +1,148 @@ +Require Import Wf. +Require Import Coq.Program.Utils. +Require Import ProofIrrelevance. + +(** 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 (proj1_sig y) (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:{ 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:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (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 <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros. + apply F_ext; auto. + intros. + rewrite (proof_irrelevance (Acc R x) r s) ; auto. + Qed. + + Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{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. + + Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := + F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) + (Acc_inv r (m (proj1_sig 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. + + Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig 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. + + Lemma Fix_measure_F_eq : + forall (x:A) (r:Acc lt (m x)), + F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (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. diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v new file mode 100644 index 0000000000..c6e5a64fb3 --- /dev/null +++ b/theories/Program/FunctionalExtensionality.v @@ -0,0 +1,65 @@ +Require Import Coq.Program.Utils. +Require Import Coq.Program.FixSub. + +(** 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 : forall A B (f g : A -> B), + (forall x, f x = g x) -> f = g. + +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. + +Hint Resolve fun_extensionality fun_extensionality_dep : program. + +(** 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. *) + +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). + apply (fun_extensionality_dep _ _ _ _ H). + rewrite H0 ; auto. +Qed. + +(** For a function defined with Program using a measure. *) + +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). + apply (fun_extensionality_dep _ _ _ _ H). + rewrite H0 ; auto. +Qed. + +Ltac apply_ext := + match goal with + [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y) + end. + + diff --git a/theories/Program/Heq.v b/theories/Program/Heq.v new file mode 100644 index 0000000000..cd405219f6 --- /dev/null +++ b/theories/Program/Heq.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 => let H' := fresh "H" in + assert (H' := JMeq_eq H) ; clear H ; rename H' into 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. + +(** 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. + diff --git a/theories/Program/Program.v b/theories/Program/Program.v new file mode 100644 index 0000000000..4dc50694fa --- /dev/null +++ b/theories/Program/Program.v @@ -0,0 +1,3 @@ +Require Export Coq.Program.Utils. +Require Export Coq.Program.FixSub. +Require Export Coq.Program.Heq. \ No newline at end of file diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v new file mode 100644 index 0000000000..d5ccdf1c5b --- /dev/null +++ b/theories/Program/Tactics.v @@ -0,0 +1,165 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + match goal with + | [H : (ex _) |- _] => tac H + | [H : (sig ?P) |- _ ] => tac 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. + +(** A non-failing subst that substitutes as much as possible. *) + +Tactic Notation "subst" "*" := + repeat (match goal with + [ H : ?X = ?Y |- _ ] => subst X || subst Y + 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 + | H : ?T |- _ => + match T with + | 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 + | |- ?T => + match T with + | 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 + 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_call_as f l := + let tac t := destruct t as l in on_call f tac. + +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. + +(** Try to inject any potential constructor equality hypothesis. *) + +Ltac autoinjection := + let tac H := inversion H ; subst ; 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. + +(** 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. + +(** 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 manner similar to + the BasicElim tactic of "Elimination with a motive" by Conor McBride. *) + +Tactic Notation "dependent" "induction" ident(H) := + generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; + induction H ; intros ; subst* ; try discriminates. + +(** This tactic also generalizes the goal by the given variables before the induction. *) + +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := + generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; + generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates. + +(** The default simplification tactic used by Program. *) + +Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; + try (solve [ red ; intros ; discriminate ]) ; auto with *. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v new file mode 100644 index 0000000000..a87eda0a26 --- /dev/null +++ b/theories/Program/Utils.v @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* let (x,y) := anonymous in P)) + (x ident, y ident) : type_scope. + +(** Generates an obligation to prove False. *) + +Notation " ! " := (False_rect _ _). + +(** Abbreviation for first projection and hiding of proofs of subset objects. *) + +Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. +Notation "( x & ? )" := (@exist _ _ x _) : core_scope. + +(** Coerces objects to their support before comparing them. *) + +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). + +(** Quantifying over subsets. *) + +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). + +Notation "'forall' { x : A | P } , Q" := + (forall x:{x:A|P}, Q) + (at level 200, x ident, right associativity). + +Require Import Coq.Bool.Sumbool. + +(** Construct a dependent disjunction from a boolean. *) + +Notation "'dec'" := (sumbool_of_bool) (at level 0). + +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) + +Notation in_right := (@right _ _ _). +Notation in_left := (@left _ _ _). + +(** 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" [ "" ]. *) + +(** The scope in which programs are typed (not their types). *) + +Delimit Scope program_scope with prg. -- cgit v1.2.3