summaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Basics.v4
-rw-r--r--theories/Program/Combinators.v2
-rw-r--r--theories/Program/Equality.v12
-rw-r--r--theories/Program/Program.v2
-rw-r--r--theories/Program/Subset.v6
-rw-r--r--theories/Program/Syntax.v2
-rw-r--r--theories/Program/Tactics.v4
-rw-r--r--theories/Program/Utils.v2
-rw-r--r--theories/Program/Wf.v6
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 15:45:39 +0000