diff options
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Basics.v | 4 | ||||
-rw-r--r-- | theories/Program/Combinators.v | 2 | ||||
-rw-r--r-- | theories/Program/Equality.v | 12 | ||||
-rw-r--r-- | theories/Program/Program.v | 2 | ||||
-rw-r--r-- | theories/Program/Subset.v | 6 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 2 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 4 | ||||
-rw-r--r-- | theories/Program/Utils.v | 2 | ||||
-rw-r--r-- | theories/Program/Wf.v | 6 |
9 files changed, 22 insertions, 18 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 7cef5c5a..22436de6 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,7 @@ Hint Unfold compose. Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. -Open Local Scope program_scope. +Local Open Scope program_scope. (** The non-dependent function space between [A] and [B]. *) diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 81316ded..dcf09251 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d408845e..323e80cc 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -290,12 +290,14 @@ 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. +Definition conditional_eq {A} (x y : A) := eq x y. + 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). + (x = y -> B) -> (conditional_eq (existT P p x) (existT P p y) -> B). 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) : - (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B). + (p = q -> conditional_eq (existT P p x) (existT P q y) -> B) -> (existT P p x = existT P q y -> B). Proof. injection 2. auto. Defined. Lemma simplification_K A (x : A) (B : x = x -> Type) : @@ -319,8 +321,10 @@ Ltac simplify_one_dep_elim_term c := | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _) | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) | eq (existT _ _ _) (existT _ _ _) -> _ => - refine (simplification_existT2 _ _ _ _ _ _ _) || refine (simplification_existT1 _ _ _ _ _ _ _ _) + | conditional_eq (existT _ _ _) (existT _ _ _) -> _ => + refine (simplification_existT2 _ _ _ _ _ _ _) || + (unfold conditional_eq; intro) | ?x = ?y -> _ => (* variables case *) (unfold x) || (unfold y) || (let hyp := fresh in intros hyp ; diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 14a7ffca..be8d9a47 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index ca4002d7..34c27ed8 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. -Open Local Scope program_scope. +Local Open Scope program_scope. (** 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. *) @@ -106,7 +106,7 @@ Ltac rewrite_match_eq H := [ |- ?T ] => match T with context [ match_eq ?A ?B ?t ?f ] => - rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H))) + rewrite (match_eq_rewrite A B t f (exist _ _ (eq_sym H))) end end. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 61d389ed..a2948074 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 9694e3fd..9aba9f53 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -310,7 +310,7 @@ 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; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in * ); subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 1885decf..94e88d57 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index a823aedd..6a030c7f 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,7 +12,7 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. -Open Local Scope program_scope. +Local Open Scope program_scope. Section Well_founded. Variable A : Type. @@ -52,7 +52,7 @@ Section Well_founded. Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)). Proof. - intro x; unfold Fix_sub in |- *. + intro x; unfold Fix_sub. rewrite <- (Fix_F_eq ). apply F_ext; intros. apply Fix_F_inv. |