aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--kernel/univ.ml16
-rw-r--r--kernel/univ.mli4
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--parsing/pptactic.ml5
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/auto.ml24
-rw-r--r--tactics/auto.mli4
-rw-r--r--theories/Init/Logic.v2
-rw-r--r--theories/Logic/ChoiceFacts.v51
-rw-r--r--theories/Logic/ClassicalFacts.v21
-rw-r--r--toplevel/cerrors.ml11
12 files changed, 116 insertions, 34 deletions
diff --git a/CHANGES b/CHANGES
index 3fb67b50b..61248cb70 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,6 +16,8 @@ Commands
generation of elimination schemes.
- Modification of the Scheme command so you can ask for the name to be
automatically computed (e.g. Scheme Induction for nat Sort Set).
+- Source of universe inconsistencies now printed when option
+ "Set Printing Universes" is activated,
Libraries
@@ -35,6 +37,8 @@ Libraries
- Loading FSets/FMap used to open unwanted scopes of integer datatypes
(see bug #1347). These scopes may need to be opened manually now.
- Few changes in Reals (lemmas on prod_f_SO now on prod_f_R0).
+- Slight restructuration and extension of the Logic library regarding choice
+ and classical logic.
Language
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1abc393b5..fd916e77b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -314,9 +314,11 @@ let merge_disc g u v =
(* Universe inconsistency: error raised when trying to enforce a relation
that would create a cycle in the graph of universes. *)
-exception UniverseInconsistency
+type order_request = Lt | Le | Eq
-let error_inconsistency () = raise UniverseInconsistency
+exception UniverseInconsistency of order_request * universe * universe
+
+let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
(* enforce_univ_leq : universe_level -> universe_level -> unit *)
(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -326,7 +328,7 @@ let enforce_univ_leq u v g =
match compare g u v with
| NLE ->
(match compare g v u with
- | LT -> error_inconsistency()
+ | LT -> error_inconsistency Le u v
| LE -> merge g v u
| NLE -> setleq g u v
| EQ -> anomaly "Univ.compare")
@@ -339,11 +341,11 @@ let enforce_univ_eq u v g =
let g = declare_univ v g in
match compare g u v with
| EQ -> g
- | LT -> error_inconsistency()
+ | LT -> error_inconsistency Eq u v
| LE -> merge g u v
| NLE ->
(match compare g v u with
- | LT -> error_inconsistency()
+ | LT -> error_inconsistency Eq u v
| LE -> merge g v u
| NLE -> merge_disc g u v
| EQ -> anomaly "Univ.compare")
@@ -355,11 +357,11 @@ let enforce_univ_lt u v g =
match compare g u v with
| LT -> g
| LE -> setlt g u v
- | EQ -> error_inconsistency()
+ | EQ -> error_inconsistency Lt u v
| NLE ->
(match compare g v u with
| NLE -> setlt g u v
- | _ -> error_inconsistency())
+ | _ -> error_inconsistency Lt u v)
(*
let enforce_univ_relation g = function
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 39505173e..6c709bc83 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -49,7 +49,9 @@ val enforce_eq : constraint_function
universes graph. It raises the exception [UniverseInconsistency] if the
constraints are not satisfiable. *)
-exception UniverseInconsistency
+type order_request = Lt | Le | Eq
+
+exception UniverseInconsistency of order_request * universe * universe
val merge_constraints : constraints -> universes -> universes
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4f5a4f42..3f7c8c3e8 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -414,8 +414,10 @@ GEXTEND Gram
| IDENT "dconcl" -> TacDestructConcl
| IDENT "superauto"; l = autoargs -> TacSuperAuto l
*)
- | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural ->
- TacDAuto (n, p)
+ | IDENT "auto"; IDENT "decomp"; p = OPT natural;
+ lems = auto_using -> TacDAuto (None,p,lems)
+ | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
+ lems = auto_using -> TacDAuto (n,p,lems)
(* Context management *)
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 52b2e5f64..c6c168d4e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -766,8 +766,9 @@ and pr_atom1 = function
| TacAuto (n,lems,db) ->
hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++
pr_auto_using pr_constr lems ++ pr_hintbases db)
- | TacDAuto (n,p) ->
- hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p)
+ | TacDAuto (n,p,lems) ->
+ hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++
+ pr_opt int p ++ pr_auto_using pr_constr lems)
(* Context management *)
| TacClear (true,[]) as t -> pr_atom0 t
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f99ce1a88..d68d125bd 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -160,7 +160,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacDestructHyp of (bool * identifier located)
| TacDestructConcl
| TacSuperAuto of (int option * reference list * bool * bool)
- | TacDAuto of int or_var option * int option
+ | TacDAuto of int or_var option * int option * 'constr list
(* Context management *)
| TacClear of bool * 'id list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b78291ecd..f07541912 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -797,23 +797,23 @@ let h_auto n lems l =
l'instant *)
let default_search_decomp = ref 1
-let destruct_auto des_opt n gl =
+let destruct_auto des_opt lems n gl =
let hyps = pf_hyps gl in
- search_gen des_opt n [searchtable_map "core"]
- (make_local_hint_db [] gl) hyps gl
+ search_gen des_opt n (List.map searchtable_map ["core";"extcore"])
+ (make_local_hint_db lems gl) hyps gl
-let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
+let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
-let default_dauto = dautomatic !default_search_decomp !default_search_depth
+let dauto (n,p) lems =
+ let p = match p with Some p -> p | None -> !default_search_decomp in
+ let n = match n with Some n -> n | None -> !default_search_depth in
+ dautomatic p lems n
-let dauto = function
- | None, None -> default_dauto
- | Some n, None -> dautomatic !default_search_decomp n
- | Some n, Some p -> dautomatic p n
- | None, Some p -> dautomatic p !default_search_depth
+let default_dauto = dauto (None,None) []
-let h_dauto (n,p) =
- Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p))
+let h_dauto (n,p) lems =
+ Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map inj_open lems))
+ (dauto (n,p) lems)
(***************************************)
(*** A new formulation of Auto *********)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0e702a65b..ac4f126f3 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -174,11 +174,11 @@ val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
(*s The following is not yet up to date -- Papageno. *)
(* DAuto *)
-val dauto : int option * int option -> tactic
+val dauto : int option * int option -> constr list -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
-val h_dauto : int option * int option -> tactic
+val h_dauto : int option * int option -> constr list -> tactic
(* SuperAuto *)
type autoArguments =
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index bdc8f9de6..8deb362cd 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -89,6 +89,8 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
End Equivalence.
+Hint Unfold iff: extcore.
+
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
either [P] and [Q], or [~P] and [Q] *)
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 75043c422..488da63b6 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -95,9 +95,9 @@ Section ChoiceSchemes.
Variables A B :Type.
-Variables P:A->Prop.
+Variable P:A->Prop.
-Variables R:A->B->Prop.
+Variable R:A->B->Prop.
(** ** Constructive choice and description *)
@@ -396,6 +396,16 @@ Proof.
intro x; apply IndPrem; eauto.
Qed.
+Lemma fun_choice_and_indep_general_prem_iff_guarded_fun_choice :
+ FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises
+ <-> GuardedFunctionalChoice.
+Proof.
+ auto decomp using
+ guarded_fun_choice_imp_indep_of_general_premises,
+ guarded_fun_choice_imp_fun_choice,
+ fun_choice_and_indep_general_prem_imp_guarded_fun_choice.
+Qed.
+
(** AC_fun + Drinker = OAC_fun *)
(** This was already observed by Bell [Bell] *)
@@ -427,6 +437,16 @@ Proof.
exists f; assumption.
Qed.
+Lemma fun_choice_and_small_drinker_iff_omniscient_fun_choice :
+ FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox
+ <-> OmniscientFunctionalChoice.
+Proof.
+ auto decomp using
+ omniscient_fun_choice_imp_small_drinker,
+ omniscient_fun_choice_imp_fun_choice,
+ fun_choice_and_small_drinker_imp_omniscient_fun_choice.
+Qed.
+
(** OAC_fun = GAC_fun *)
(** This is derivable from the intuitionistic equivalence between IGP and Drinker
@@ -614,6 +634,14 @@ Proof.
destruct Heq using eq_indd; trivial.
Qed.
+Theorem dep_iff_non_dep_functional_rel_reification :
+ FunctionalRelReification <-> DependentFunctionalRelReification.
+Proof.
+ auto decomp using
+ non_dep_dep_functional_rel_reification,
+ dep_non_dep_functional_rel_reification.
+Qed.
+
(**********************************************************************)
(** * Non contradiction of constructive descriptions wrt functional axioms of choice *)
@@ -649,10 +677,10 @@ Qed.
(** ** Non contradiction of definite description *)
Lemma relative_non_contradiction_of_definite_descr :
- (ConstructiveDefiniteDescription -> False)
- -> (FunctionalRelReification -> False).
+ forall C:Prop, (ConstructiveDefiniteDescription -> C)
+ -> (FunctionalRelReification -> C).
Proof.
- intros H FunReify.
+ intros C H FunReify.
assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify).
pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}).
pose (B0 := fun x:A0 => projT1 x).
@@ -675,6 +703,19 @@ Proof.
apply (proj2_sig (DefDescr B (R x) (H x))).
Qed.
+(** Remark, the following lemma morally holds:
+
+Definition In_propositional_context (A:Type) := forall C:Prop, (A -> C) -> C.
+
+Lemma constructive_definite_descr_in_prop_context_iff_fun_reification :
+ In_propositional_context ConstructiveDefiniteDescription
+ <-> FunctionalRelReification.
+
+but expecting [FunctionalRelReification] to be applied on the same
+Type universes on both sides of the equivalence breaks the
+stratification of universes.
+*)
+
(**********************************************************************)
(** * Excluded-middle + definite description => computational excluded-middle *)
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index ad9171843..f3f177a73 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -91,6 +91,17 @@ Proof.
right; apply (Ext A False); split; [ exact H | apply False_ind ].
Qed.
+(** A weakest form of propositional extensionality: extensionality for
+ provable propositions only *)
+
+Definition provable_prop_extensionality := forall A:Prop, A -> A = True.
+
+Lemma provable_prop_ext :
+ prop_extensionality -> provable_prop_extensionality.
+Proof.
+ intros Ext A Ha; apply Ext; split; trivial.
+Qed.
+
(************************************************************************)
(** * Classical logic and proof-irrelevance *)
@@ -105,6 +116,7 @@ Qed.
(just take the identity), which
implies the existence of a fixpoint operator in [A]
(e.g. take the Y combinator of lambda-calculus)
+
*)
Definition inhabited (A:Prop) := A.
@@ -143,6 +155,10 @@ Proof.
reflexivity.
Qed.
+(** Remark: [prop_extensionality] can be replaced in lemma [ext_prop_fixpoint]
+ by the weakest property [provable_prop_extensionality].
+*)
+
(************************************************************************)
(** ** CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *)
@@ -230,6 +246,11 @@ Section Proof_irrelevance_Prop_Ext_CC.
End Proof_irrelevance_Prop_Ext_CC.
+(** Remark: [prop_extensionality] can be replaced in lemma
+ [ext_prop_dep_proof_irrel_gen] by the weakest property
+ [provable_prop_extensionality].
+*)
+
(************************************************************************)
(** ** CIC |- prop. ext. -> proof-irrelevance *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4c600bc66..832e444ca 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -64,8 +64,15 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
| Sys.Break ->
hov 0 (fnl () ++ str "User interrupt.")
- | Univ.UniverseInconsistency ->
- hov 0 (str "Error: Universe inconsistency.")
+ | Univ.UniverseInconsistency (o,u,v) ->
+ let msg =
+ if !Constrextern.print_universes then
+ spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
+ str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
+ ++ spc() ++ Univ.pr_uni v ++ str")"
+ else
+ mt() in
+ hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
| PretypeError(ctx,te) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:52:58 +0000