diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 10 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 4 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 108 | ||||
| -rw-r--r-- | theories/Program/Program.v | 6 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 4 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 47 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 26 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 4 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 4 |
9 files changed, 81 insertions, 132 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 37c4d94d..7cef5c5a 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,13 +1,11 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Basics.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Standard functions and combinators. Proofs about them require functional extensionality and can be found @@ -19,7 +17,7 @@ (** The polymorphic identity function is defined in [Datatypes]. *) -Implicit Arguments id [[A]]. +Arguments id {A} x. (** Function composition. *) @@ -55,5 +53,5 @@ 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]]. +Arguments prod_curry {A B C} f p. +Arguments prod_uncurry {A B C} f x y. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index f446b455..81316ded 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,13 +1,11 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Combinators.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** * Proofs about standard combinators, exports functional extensionality. Author: Matthieu Sozeau diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index f63aad43..06ff7cd1 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Tactics related to (dependent) equality and proof irrelevance. *) Require Export ProofIrrelevance. @@ -15,9 +13,6 @@ Require Export JMeq. Require Import Coq.Program.Tactics. -Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. - Ltac is_ground_goal := match goal with |- ?T => is_ground T @@ -33,18 +28,12 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. -Ltac unblock_goal := unfold block at 1. -Ltac unblock_all := unfold block in *. +Ltac unblock_goal := cbv beta delta [block]. (** Notation for heterogenous equality. *) Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). -(** Notation for the single element of [x = x] and [x ~= x]. *) - -Implicit Arguments eq_refl [[A] [x]] [A]. -Implicit Arguments JMeq_refl [[A] [x]] [A]. - (** Do something on an heterogeneous equality appearing in the context. *) Ltac on_JMeq tac := @@ -177,15 +166,15 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. intros. apply proof_irrelevance. Qed. +Proof. apply proof_irrelevance. Qed. -Lemma UIP_refl_refl : Π A (x : A), +Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. -Proof. intros. apply UIP_refl. Qed. +Proof. apply UIP_refl. Qed. -Lemma inj_pairT2_refl : Π A (x : A) (P : A -> Type) (p : P x), +Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) : Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. -Proof. intros. apply UIP_refl. Qed. +Proof. apply UIP_refl. Qed. Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. @@ -225,7 +214,7 @@ Ltac simplify_eqs := Ltac simplify_IH_hyps := repeat match goal with - | [ hyp : context [ block _ ] |- _ ] => specialize_eqs hyp ; unfold block in hyp + | [ hyp : _ |- _ ] => specialize_eqs hyp end. (** We split substitution tactics in the two directions depending on which @@ -285,27 +274,31 @@ Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p. (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *) -Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x). -Proof. intros; subst. apply X. Defined. +Lemma solution_left A (B : A -> Type) (t : A) : + B t -> (forall x, x = t -> B x). +Proof. intros; subst; assumption. Defined. -Lemma solution_right : Π A (B : A -> Type) (t : A), B t -> (Π x, t = x -> B x). -Proof. intros; subst; apply X. Defined. +Lemma solution_right A (B : A -> Type) (t : A) : + B t -> (forall x, t = x -> B x). +Proof. intros; subst; assumption. Defined. -Lemma deletion : Π A B (t : A), B -> (t = t -> B). +Lemma deletion A B (t : A) : B -> (t = t -> B). Proof. intros; assumption. Defined. -Lemma simplification_heq : Π A B (x y : A), (x = y -> B) -> (JMeq x y -> B). -Proof. intros; apply X; apply (JMeq_eq H). Defined. +Lemma simplification_heq A B (x y : A) : + (x = y -> B) -> (JMeq x y -> B). +Proof. intros H J; apply H; apply (JMeq_eq J). Defined. -Lemma simplification_existT2 : Π A (P : A -> Type) B (p : A) (x y : P p), +Lemma simplification_existT2 A (P : A -> Type) B (p : A) (x y : P p) : (x = y -> B) -> (existT P p x = existT P p y -> B). -Proof. intros. apply X. apply inj_pair2. exact H. Defined. +Proof. intros H E. apply H. apply inj_pair2. assumption. Defined. -Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q), +Lemma simplification_existT1 A (P : A -> Type) B (p q : A) (x : P p) (y : P q) : (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B). -Proof. intros. injection H. intros ; auto. Defined. - -Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B eq_refl -> (Π p : x = x, B p). +Proof. injection 2. auto. Defined. + +Lemma simplification_K A (x : A) (B : x = x -> Type) : + B eq_refl -> (forall p : x = x, B p). Proof. intros. rewrite (UIP_refl A). assumption. Defined. (** This hint database and the following tactic can be used with [autounfold] to @@ -320,35 +313,20 @@ Hint Unfold solution_left solution_right deletion simplification_heq constructor forms). Compare with the lemma 16 of the paper. We don't have a [noCycle] procedure yet. *) -Ltac block_equality id := - match type of id with - | @eq ?A ?t ?u => change (block (@eq A t u)) in id - | _ => idtac - end. - -Ltac revert_blocking_until id := - Tactics.on_last_hyp ltac:(fun id' => - match id' with - | id => idtac - | _ => block_equality id' ; revert id' ; revert_blocking_until id - end). - Ltac simplify_one_dep_elim_term c := match c with | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _) | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) - | eq (existT _ ?p _) (existT _ ?q _) -> _ => + | eq (existT _ _ _) (existT _ _ _) -> _ => refine (simplification_existT2 _ _ _ _ _ _ _) || - match goal with - | H : p = q |- _ => intro - | _ => refine (simplification_existT1 _ _ _ _ _ _ _ _) - end + refine (simplification_existT1 _ _ _ _ _ _ _ _) | ?x = ?y -> _ => (* variables case *) + (unfold x) || (unfold y) || (let hyp := fresh in intros hyp ; - move hyp before x ; revert_blocking_until hyp ; generalize dependent x ; + move hyp before x ; revert_until hyp ; generalize dependent x ; refine (solution_left _ _ _ _)(* ; intros until 0 *)) || (let hyp := fresh in intros hyp ; - move hyp before y ; revert_blocking_until hyp ; generalize dependent y ; + move hyp before y ; revert_until hyp ; generalize dependent y ; refine (solution_right _ _ _ _)(* ; intros until 0 *)) | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) | ?t = ?u -> _ => let hyp := fresh in @@ -406,18 +384,18 @@ Tactic Notation "intro_block_id" ident(H) := (is_introduced H ; block_goal ; revert_until H) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_all. +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. Ltac do_intros H := (try intros until H) ; (intro_block_id H || intro_block H). -Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; block_goal ; tac H ; unblock_goal. +Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H. Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. Ltac do_depind tac H := - do_intros H ; generalize_eqs_vars H ; block_goal ; tac H ; - unblock_goal ; simplify_dep_elim ; simplify_IH_hyps ; unblock_all. + (try intros until H) ; intro_block H ; + generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. (** To dependent elimination on some hyp. *) @@ -433,26 +411,26 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id. (** A variant where generalized variables should be given by the user. *) -Ltac do_depelim' tac H := - (try intros until H) ; block_goal ; generalize_eqs H ; block_goal ; tac H ; unblock_goal ; - simplify_dep_elim ; simplify_IH_hyps ; unblock_all. +Ltac do_depelim' rev tac H := + (try intros until H) ; block_goal ; rev H ; generalize_eqs H ; tac H ; simplify_dep_elim ; + simplify_IH_hyps ; unblock_goal. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) Tactic Notation "dependent" "destruction" ident(H) := - do_depelim' ltac:(fun hyp => do_case hyp) H. + do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H. Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := - do_depelim' ltac:(fun hyp => destruct hyp using c) H. + do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H. (** This tactic also generalizes the goal by the given variables before the elimination. *) Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := - do_depelim' ltac:(fun hyp => revert l ; do_case hyp) H. + do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H. Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := - do_depelim' ltac:(fun hyp => revert l ; destruct hyp using c) H. + do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before @@ -467,7 +445,7 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := (** 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_depelim' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H. + do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H. Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := - do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H. + do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 2b6dd864..14a7ffca 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,16 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Program.v 14641 2011-11-06 11:59:10Z herbelin $ *) - 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 +Require Export Coq.Program.Syntax. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index d0a76d3f..ca4002d7 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Subset.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Tactics related to subsets and proof irrelevance. *) Require Import Coq.Program.Utils. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 582bc461..61d389ed 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Syntax.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Custom notations and implicits for Coq prelude definitions. Author: Matthieu Sozeau @@ -20,48 +18,23 @@ Notation " () " := tt. (** Set maximally inserted implicit arguments for standard definitions. *) -Implicit Arguments Some [[A]]. -Implicit Arguments None [[A]]. - -Implicit Arguments inl [[A] [B]] [A]. -Implicit Arguments inr [[A] [B]] [B]. - -Implicit Arguments left [[A] [B]] [A]. -Implicit Arguments right [[A] [B]] [B]. - -Implicit Arguments pair [[A] [B]]. -Implicit Arguments fst [[A] [B]]. -Implicit Arguments snd [[A] [B]]. - -Require Import Coq.Lists.List. +Arguments Some {A} _. +Arguments None {A}. -Implicit Arguments nil [[A]]. -Implicit Arguments cons [[A]]. +Arguments pair {A B} _ _. +Arguments fst {A B} _. +Arguments snd {A B} _. -(** Standard notations for lists. *) +Arguments nil {A}. +Arguments cons {A} _ _. -Notation " [ ] " := nil : list_scope. -Notation " [ x ] " := (cons x nil) : list_scope. -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. - -(** Implicit arguments for vectors. *) +Require List. +Export List.ListNotations. Require Import Bvector. -Implicit Arguments Vnil [[A]] []. -Implicit Arguments Vcons [[A] [n]] []. - (** Treating 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 "exists" constr(x) := exists x. Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y. Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index f62ff703..9694e3fd 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -61,12 +59,20 @@ 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 + let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in + (destruct H as [H ph ph']) + in let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in + let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in + (destruct H as [H ph ph']) + in match goal with | [H : (ex _) |- _] => tac H | [H : (sig ?P) |- _ ] => tac H | [H : (sigT ?P) |- _ ] => tacT H - | [H : (ex2 _) |- _] => tac H + | [H : (ex2 _ _) |- _] => tac2 H + | [H : (sig2 ?P _) |- _ ] => tac2 H + | [H : (sigT2 ?P _) |- _ ] => tacT2 H end. (** Repeateadly destruct existentials. *) @@ -304,18 +310,22 @@ Ltac refine_hyp c := possibly using [program_simplify] to use standard goal-cleaning tactics. *) Ltac program_simplify := - simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in *); +simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in * ); subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -(** We only try to solve proposition goals automatically. *) +(** Restrict automation to propositional obligations. *) -Ltac program_solve := +Ltac program_solve_wf := match goal with | |- well_founded _ => auto with * | |- ?T => match type of T with Prop => auto end end. -Ltac program_simpl := program_simplify ; try program_solve. +Create HintDb program discriminated. + +Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf. Obligation Tactic := program_simpl. + +Definition obligation (A : Type) {a : A} := a.
\ No newline at end of file diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 1e57a74b..1885decf 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Utils.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Various syntaxic shortands that are useful with [Program]. *) Require Export Coq.Program.Tactics. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 3afaf5e8..a823aedd 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) |