summaryrefslogtreecommitdiff
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/Omega.v4
-rw-r--r--plugins/omega/OmegaLemmas.v9
-rw-r--r--plugins/omega/OmegaPlugin.v4
-rw-r--r--plugins/omega/PreOmega.v115
-rw-r--r--plugins/omega/coq_omega.ml357
-rw-r--r--plugins/omega/g_omega.ml44
-rw-r--r--plugins/omega/omega.ml4
7 files changed, 227 insertions, 270 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index c8a06265..3f9d0f44 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* 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 *)
@@ -13,8 +13,6 @@
(* *)
(**************************************************************************)
-(* $Id: Omega.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
Require Export ZArith_base.
Require Export OmegaLemmas.
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index ec9faedd..5b6f4670 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i $Id: OmegaLemmas.v 12337 2009-09-17 15:58:14Z glondu $ i*)
-
Require Import ZArith_base.
Open Local Scope Z_scope.
@@ -300,3 +298,10 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
(H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
+
+Theorem intro_Z :
+ forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+ intros n; exists (Z_of_nat n); split; trivial.
+ rewrite Zmult_1_r, Zplus_0_r. apply Zle_0_nat.
+Qed.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 69a6ea72..a3ab34a9 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -1,11 +1,9 @@
(************************************************************************)
(* 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: OmegaPlugin.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
Declare ML Module "omega_plugin".
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index a5a085a9..46fd5682 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -28,7 +28,7 @@ Open Local Scope Z_scope.
Ltac zify_unop_core t thm a :=
(* Let's introduce the specification theorem for t *)
- let H:= fresh "H" in assert (H:=thm a);
+ pose proof (thm a);
(* Then we replace (t a) everywhere with a fresh variable *)
let z := fresh "z" in set (z:=t a) in *; clearbody z.
@@ -159,11 +159,9 @@ Ltac zify_nat_op :=
(* mult -> Zmult and a positivity hypothesis *)
| H : context [ Z_of_nat (mult ?a ?b) ] |- _ =>
- let H:= fresh "H" in
- assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+ pose proof (Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
| |- context [ Z_of_nat (mult ?a ?b) ] =>
- let H:= fresh "H" in
- assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+ pose proof (Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
(* O -> Z0 *)
| H : context [ Z_of_nat O ] |- _ => simpl (Z_of_nat O) in H
@@ -184,20 +182,9 @@ Ltac zify_nat_op :=
end
(* atoms of type nat : we add a positivity condition (if not already there) *)
- | H : context [ Z_of_nat ?a ] |- _ =>
- match goal with
- | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
- | H' : 0 <= Z_of_nat' a |- _ => fail
- | _ => let H:= fresh "H" in
- assert (H:=Zle_0_nat a); hide_Z_of_nat a
- end
- | |- context [ Z_of_nat ?a ] =>
- match goal with
- | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
- | H' : 0 <= Z_of_nat' a |- _ => fail
- | _ => let H:= fresh "H" in
- assert (H:=Zle_0_nat a); hide_Z_of_nat a
- end
+ | _ : 0 <= Z_of_nat ?a |- _ => hide_Z_of_nat a
+ | _ : context [ Z_of_nat ?a ] |- _ => pose proof (Zle_0_nat a); hide_Z_of_nat a
+ | |- context [ Z_of_nat ?a ] => pose proof (Zle_0_nat a); hide_Z_of_nat a
end.
Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
@@ -223,17 +210,17 @@ Ltac zify_positive_rel :=
| H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
| |- context [ @eq positive ?a ?b ] => rewrite (Zpos_eq_iff a b)
(* II: less than *)
- | H : context [ (?a<?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
- | |- context [ (?a<?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
+ | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
+ | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
(* III: less or equal *)
- | H : context [ (?a<=?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
- | |- context [ (?a<=?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
+ | H : context [ (?a <= ?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
+ | |- context [ (?a <= ?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
(* IV: greater than *)
- | H : context [ (?a>?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
- | |- context [ (?a>?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
+ | H : context [ (?a > ?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
+ | |- context [ (?a > ?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
(* V: greater or equal *)
- | H : context [ (?a>=?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
- | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
+ | H : context [ (?a >= ?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
+ | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
end.
Ltac zify_positive_op :=
@@ -282,11 +269,9 @@ Ltac zify_positive_op :=
(* Pmult -> Zmult and a positivity hypothesis *)
| H : context [ Zpos (Pmult ?a ?b) ] |- _ =>
- let H:= fresh "H" in
- assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+ pose proof (Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
| |- context [ Zpos (Pmult ?a ?b) ] =>
- let H:= fresh "H" in
- assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+ pose proof (Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
(* xO *)
| H : context [ Zpos (xO ?a) ] |- _ =>
@@ -320,18 +305,9 @@ Ltac zify_positive_op :=
| |- context [ Zpos xH ] => hide_Zpos xH
(* atoms of type positive : we add a positivity condition (if not already there) *)
- | H : context [ Zpos ?a ] |- _ =>
- match goal with
- | H' : Zpos a > 0 |- _ => hide_Zpos a
- | H' : Zpos' a > 0 |- _ => fail
- | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
- end
- | |- context [ Zpos ?a ] =>
- match goal with
- | H' : Zpos a > 0 |- _ => hide_Zpos a
- | H' : Zpos' a > 0 |- _ => fail
- | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
- end
+ | _ : Zpos ?a > 0 |- _ => hide_Zpos a
+ | _ : context [ Zpos ?a ] |- _ => pose proof (Zgt_pos_0 a); hide_Zpos a
+ | |- context [ Zpos ?a ] => pose proof (Zgt_pos_0 a); hide_Zpos a
end.
Ltac zify_positive :=
@@ -358,25 +334,25 @@ Ltac zify_N_rel :=
| H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
| |- context [ @eq N ?a ?b ] => rewrite (Z_of_N_eq_iff a b)
(* II: less than *)
- | H : (?a<?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
- | |- (?a<?b)%N => apply (Z_of_N_lt_rev a b)
- | H : context [ (?a<?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
- | |- context [ (?a<?b)%N ] => rewrite (Z_of_N_lt_iff a b)
+ | H : (?a < ?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
+ | |- (?a < ?b)%N => apply (Z_of_N_lt_rev a b)
+ | H : context [ (?a < ?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
+ | |- context [ (?a < ?b)%N ] => rewrite (Z_of_N_lt_iff a b)
(* III: less or equal *)
- | H : (?a<=?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
- | |- (?a<=?b)%N => apply (Z_of_N_le_rev a b)
- | H : context [ (?a<=?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
- | |- context [ (?a<=?b)%N ] => rewrite (Z_of_N_le_iff a b)
+ | H : (?a <= ?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
+ | |- (?a <= ?b)%N => apply (Z_of_N_le_rev a b)
+ | H : context [ (?a <= ?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
+ | |- context [ (?a <= ?b)%N ] => rewrite (Z_of_N_le_iff a b)
(* IV: greater than *)
- | H : (?a>?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
- | |- (?a>?b)%N => apply (Z_of_N_gt_rev a b)
- | H : context [ (?a>?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
- | |- context [ (?a>?b)%N ] => rewrite (Z_of_N_gt_iff a b)
+ | H : (?a > ?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
+ | |- (?a > ?b)%N => apply (Z_of_N_gt_rev a b)
+ | H : context [ (?a > ?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
+ | |- context [ (?a > ?b)%N ] => rewrite (Z_of_N_gt_iff a b)
(* V: greater or equal *)
- | H : (?a>=?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
- | |- (?a>=?b)%N => apply (Z_of_N_ge_rev a b)
- | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
- | |- context [ (?a>=?b)%N ] => rewrite (Z_of_N_ge_iff a b)
+ | H : (?a >= ?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
+ | |- (?a >= ?b)%N => apply (Z_of_N_ge_rev a b)
+ | H : context [ (?a >= ?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
+ | |- context [ (?a >= ?b)%N ] => rewrite (Z_of_N_ge_iff a b)
end.
Ltac zify_N_op :=
@@ -413,25 +389,14 @@ Ltac zify_N_op :=
(* Nmult -> Zmult and a positivity hypothesis *)
| H : context [ Z_of_N (Nmult ?a ?b) ] |- _ =>
- let H:= fresh "H" in
- assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+ pose proof (Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
| |- context [ Z_of_N (Nmult ?a ?b) ] =>
- let H:= fresh "H" in
- assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+ pose proof (Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
(* atoms of type N : we add a positivity condition (if not already there) *)
- | H : context [ Z_of_N ?a ] |- _ =>
- match goal with
- | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
- | H' : 0 <= Z_of_N' a |- _ => fail
- | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
- end
- | |- context [ Z_of_N ?a ] =>
- match goal with
- | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
- | H' : 0 <= Z_of_N' a |- _ => fail
- | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
- end
+ | _ : 0 <= Z_of_N ?a |- _ => hide_Z_of_N a
+ | _ : context [ Z_of_N ?a ] |- _ => pose proof (Z_of_N_le_0 a); hide_Z_of_N a
+ | |- context [ Z_of_N ?a ] => pose proof (Z_of_N_le_0 a); hide_Z_of_N a
end.
Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 20565d06..d7dfe149 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* 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 *)
@@ -13,8 +13,6 @@
(* *)
(**************************************************************************)
-(* $Id: coq_omega.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Pp
open Reduction
@@ -22,7 +20,6 @@ open Proof_type
open Names
open Nameops
open Term
-open Termops
open Declarations
open Environ
open Sign
@@ -60,6 +57,7 @@ open Goptions
let _ =
declare_bool_option
{ optsync = false;
+ optdepr = false;
optname = "Omega system time displaying flag";
optkey = ["Omega";"System"];
optread = read display_system_flag;
@@ -68,6 +66,7 @@ let _ =
let _ =
declare_bool_option
{ optsync = false;
+ optdepr = false;
optname = "Omega action display flag";
optkey = ["Omega";"Action"];
optread = read display_action_flag;
@@ -76,6 +75,7 @@ let _ =
let _ =
declare_bool_option
{ optsync = false;
+ optdepr = false;
optname = "Omega old style flag";
optkey = ["Omega";"OldStyle"];
optread = read old_style_flag;
@@ -128,12 +128,12 @@ let intern_id,unintern_id =
let mk_then = tclTHENLIST
-let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
+let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c])
let generalize_tac t = generalize_time (generalize t)
let elim t = elim_time (simplest_elim t)
let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s]
let rev_assoc k =
let rec loop = function
@@ -150,7 +150,7 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag =
let hide_constr,find_constr,clear_tables,dump_tables =
let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
(fun h id eg b -> l := (h,(id,eg,b)):: !l),
- (fun h -> try List.assoc h !l with Not_found -> failwith "find_contr"),
+ (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"),
(fun () -> l := []),
(fun () -> !l)
@@ -169,6 +169,8 @@ let coq_modules =
let init_constant = gen_constant_in_modules "Omega" init_modules
let constant = gen_constant_in_modules "Omega" coq_modules
+let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]]
+
(* Zarith *)
let coq_xH = lazy (constant "xH")
let coq_xO = lazy (constant "xO")
@@ -184,6 +186,7 @@ let coq_Zmult = lazy (constant "Zmult")
let coq_Zopp = lazy (constant "Zopp")
let coq_Zminus = lazy (constant "Zminus")
let coq_Zsucc = lazy (constant "Zsucc")
+let coq_Zpred = lazy (constant "Zpred")
let coq_Zgt = lazy (constant "Zgt")
let coq_Zle = lazy (constant "Zle")
let coq_Z_of_nat = lazy (constant "Z_of_nat")
@@ -191,13 +194,13 @@ let coq_inj_plus = lazy (constant "inj_plus")
let coq_inj_mult = lazy (constant "inj_mult")
let coq_inj_minus1 = lazy (constant "inj_minus1")
let coq_inj_minus2 = lazy (constant "inj_minus2")
-let coq_inj_S = lazy (constant "inj_S")
-let coq_inj_le = lazy (constant "inj_le")
-let coq_inj_lt = lazy (constant "inj_lt")
-let coq_inj_ge = lazy (constant "inj_ge")
-let coq_inj_gt = lazy (constant "inj_gt")
-let coq_inj_neq = lazy (constant "inj_neq")
-let coq_inj_eq = lazy (constant "inj_eq")
+let coq_inj_S = lazy (z_constant "inj_S")
+let coq_inj_le = lazy (z_constant "Znat.inj_le")
+let coq_inj_lt = lazy (z_constant "Znat.inj_lt")
+let coq_inj_ge = lazy (z_constant "Znat.inj_ge")
+let coq_inj_gt = lazy (z_constant "Znat.inj_gt")
+let coq_inj_neq = lazy (z_constant "inj_neq")
+let coq_inj_eq = lazy (z_constant "inj_eq")
let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse")
let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
@@ -255,6 +258,7 @@ let coq_dec_Zgt = lazy (constant "dec_Zgt")
let coq_dec_Zge = lazy (constant "dec_Zge")
let coq_not_Zeq = lazy (constant "not_Zeq")
+let coq_not_Zne = lazy (constant "not_Zne")
let coq_Znot_le_gt = lazy (constant "Znot_le_gt")
let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
@@ -323,6 +327,7 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
| _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
let sp_Zsucc = lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
+let sp_Zpred = lazy (evaluable_ref_of_constr "Zpred" coq_Zpred)
let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
@@ -356,7 +361,7 @@ let mk_integer n =
[| loop (abs n) |])
type omega_constant =
- | Zplus | Zmult | Zminus | Zsucc | Zopp
+ | Zplus | Zmult | Zminus | Zsucc | Zopp | Zpred
| Plus | Mult | Minus | Pred | S | O
| Zpos | Zneg | Z0 | Z_of_nat
| Eq | Neq
@@ -376,32 +381,39 @@ type result =
| Kimp of constr * constr
| Kufo
+(* Nota: Kimp correspond to a binder (Prod), but hopefully we won't
+ have to bother with term lifting: Kimp will correspond to anonymous
+ product, for which (Rel 1) doesn't occur in the right term.
+ Moreover, we'll work on fully introduced goals, hence no Rel's in
+ the term parts that we manipulate, but rather Var's.
+ Said otherwise: all constr manipulated here are closed *)
+
let destructurate_prop t =
let c, args = decompose_app t in
match kind_of_term c, args with
- | _, [_;_;_] when c = build_coq_eq () -> Kapp (Eq,args)
- | _, [_;_] when c = Lazy.force coq_neq -> Kapp (Neq,args)
- | _, [_;_] when c = Lazy.force coq_Zne -> Kapp (Zne,args)
- | _, [_;_] when c = Lazy.force coq_Zle -> Kapp (Zle,args)
- | _, [_;_] when c = Lazy.force coq_Zlt -> Kapp (Zlt,args)
- | _, [_;_] when c = Lazy.force coq_Zge -> Kapp (Zge,args)
- | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
- | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
- | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
- | _, [_;_] when c = Lazy.force coq_iff -> Kapp (Iff, args)
- | _, [_] when c = build_coq_not () -> Kapp (Not,args)
- | _, [] when c = build_coq_False () -> Kapp (False,args)
- | _, [] when c = build_coq_True () -> Kapp (True,args)
- | _, [_;_] when c = Lazy.force coq_le -> Kapp (Le,args)
- | _, [_;_] when c = Lazy.force coq_lt -> Kapp (Lt,args)
- | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
- | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
+ | _, [_;_;_] when eq_constr c (build_coq_eq ()) -> Kapp (Eq,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args)
+ | _, [_;_] when eq_constr c (build_coq_and ()) -> Kapp (And,args)
+ | _, [_;_] when eq_constr c (build_coq_or ()) -> Kapp (Or,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args)
+ | _, [_] when eq_constr c (build_coq_not ()) -> Kapp (Not,args)
+ | _, [] when eq_constr c (build_coq_False ()) -> Kapp (False,args)
+ | _, [] when eq_constr c (build_coq_True ()) -> Kapp (True,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args)
| Const sp, args ->
- Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args)
+ Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args)
| Construct csp , args ->
- Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args)
+ Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args)
| Ind isp, args ->
- Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args)
+ Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
| Var id,[] -> Kvar id
| Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
| Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
@@ -410,43 +422,44 @@ let destructurate_prop t =
let destructurate_type t =
let c, args = decompose_app t in
match kind_of_term c, args with
- | _, [] when c = Lazy.force coq_Z -> Kapp (Z,args)
- | _, [] when c = Lazy.force coq_nat -> Kapp (Nat,args)
+ | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args)
+ | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args)
| _ -> Kufo
let destructurate_term t =
let c, args = decompose_app t in
match kind_of_term c, args with
- | _, [_;_] when c = Lazy.force coq_Zplus -> Kapp (Zplus,args)
- | _, [_;_] when c = Lazy.force coq_Zmult -> Kapp (Zmult,args)
- | _, [_;_] when c = Lazy.force coq_Zminus -> Kapp (Zminus,args)
- | _, [_] when c = Lazy.force coq_Zsucc -> Kapp (Zsucc,args)
- | _, [_] when c = Lazy.force coq_Zopp -> Kapp (Zopp,args)
- | _, [_;_] when c = Lazy.force coq_plus -> Kapp (Plus,args)
- | _, [_;_] when c = Lazy.force coq_mult -> Kapp (Mult,args)
- | _, [_;_] when c = Lazy.force coq_minus -> Kapp (Minus,args)
- | _, [_] when c = Lazy.force coq_pred -> Kapp (Pred,args)
- | _, [_] when c = Lazy.force coq_S -> Kapp (S,args)
- | _, [] when c = Lazy.force coq_O -> Kapp (O,args)
- | _, [_] when c = Lazy.force coq_Zpos -> Kapp (Zneg,args)
- | _, [_] when c = Lazy.force coq_Zneg -> Kapp (Zpos,args)
- | _, [] when c = Lazy.force coq_Z0 -> Kapp (Z0,args)
- | _, [_] when c = Lazy.force coq_Z_of_nat -> Kapp (Z_of_nat,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args)
+ | _, [_] when eq_constr c (Lazy.force coq_Zsucc) -> Kapp (Zsucc,args)
+ | _, [_] when eq_constr c (Lazy.force coq_Zpred) -> Kapp (Zpred,args)
+ | _, [_] when eq_constr c (Lazy.force coq_Zopp) -> Kapp (Zopp,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_plus) -> Kapp (Plus,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_mult) -> Kapp (Mult,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_minus) -> Kapp (Minus,args)
+ | _, [_] when eq_constr c (Lazy.force coq_pred) -> Kapp (Pred,args)
+ | _, [_] when eq_constr c (Lazy.force coq_S) -> Kapp (S,args)
+ | _, [] when eq_constr c (Lazy.force coq_O) -> Kapp (O,args)
+ | _, [_] when eq_constr c (Lazy.force coq_Zpos) -> Kapp (Zneg,args)
+ | _, [_] when eq_constr c (Lazy.force coq_Zneg) -> Kapp (Zpos,args)
+ | _, [] when eq_constr c (Lazy.force coq_Z0) -> Kapp (Z0,args)
+ | _, [_] when eq_constr c (Lazy.force coq_Z_of_nat) -> Kapp (Z_of_nat,args)
| Var id,[] -> Kvar id
| _ -> Kufo
let recognize_number t =
let rec loop t =
match decompose_app t with
- | f, [t] when f = Lazy.force coq_xI -> one + two * loop t
- | f, [t] when f = Lazy.force coq_xO -> two * loop t
- | f, [] when f = Lazy.force coq_xH -> one
+ | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t
+ | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t
+ | f, [] when eq_constr f (Lazy.force coq_xH) -> one
| _ -> failwith "not a number"
in
match decompose_app t with
- | f, [t] when f = Lazy.force coq_Zpos -> loop t
- | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t)
- | f, [] when f = Lazy.force coq_Z0 -> zero
+ | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t
+ | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t)
+ | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero
| _ -> failwith "not a number"
type constr_path =
@@ -891,6 +904,10 @@ let rec transform p t =
let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
[| t1; mk_integer one |])) in
unfold sp_Zsucc :: tac,t
+ | Kapp(Zpred,[t1]) ->
+ let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+ [| t1; mk_integer negone |])) in
+ unfold sp_Zpred :: tac,t
| Kapp(Zmult,[t1;t2]) ->
let tac1,t1' = transform (P_APP 1 :: p) t1
and tac2,t2' = transform (P_APP 2 :: p) t2 in
@@ -1548,6 +1565,38 @@ let nat_inject gl =
in
loop (List.rev (pf_hyps_types gl)) gl
+let dec_binop = function
+ | Zne -> coq_dec_Zne
+ | Zle -> coq_dec_Zle
+ | Zlt -> coq_dec_Zlt
+ | Zge -> coq_dec_Zge
+ | Zgt -> coq_dec_Zgt
+ | Le -> coq_dec_le
+ | Lt -> coq_dec_lt
+ | Ge -> coq_dec_ge
+ | Gt -> coq_dec_gt
+ | _ -> raise Not_found
+
+let not_binop = function
+ | Zne -> coq_not_Zne
+ | Zle -> coq_Znot_le_gt
+ | Zlt -> coq_Znot_lt_ge
+ | Zge -> coq_Znot_ge_lt
+ | Zgt -> coq_Znot_gt_le
+ | Le -> coq_not_le
+ | Lt -> coq_not_lt
+ | Ge -> coq_not_ge
+ | Gt -> coq_not_gt
+ | _ -> raise Not_found
+
+(** A decidability check : for some [t], could we build a term
+ of type [decidable t] (i.e. [t\/~t]) ? Otherwise, we raise
+ [Undecidable]. Note that a successful check implies that
+ [t] has type Prop.
+*)
+
+exception Undecidable
+
let rec decidability gl t =
match destructurate_prop t with
| Kapp(Or,[t1;t2]) ->
@@ -1560,34 +1609,24 @@ let rec decidability gl t =
mkApp (Lazy.force coq_dec_iff, [| t1; t2;
decidability gl t1; decidability gl t2 |])
| Kimp(t1,t2) ->
- mkApp (Lazy.force coq_dec_imp, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
- | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1;
- decidability gl t1 |])
+ (* This is the only situation where it's not obvious that [t]
+ is in Prop. The recursive call on [t2] will ensure that. *)
+ mkApp (Lazy.force coq_dec_imp,
+ [| t1; t2; decidability gl t1; decidability gl t2 |])
+ | Kapp(Not,[t1]) ->
+ mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
| Kapp(Eq,[typ;t1;t2]) ->
begin match destructurate_type (pf_nf gl typ) with
| Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
| Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
- | _ -> errorlabstrm "decidability"
- (str "Omega: Can't solve a goal with equality on " ++
- Printer.pr_lconstr typ)
+ | _ -> raise Undecidable
end
- | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
- | Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
- | Kapp(Zlt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zlt, [| t1;t2 |])
- | Kapp(Zge,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zge, [| t1;t2 |])
- | Kapp(Zgt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zgt, [| t1;t2 |])
- | Kapp(Le, [t1;t2]) -> mkApp (Lazy.force coq_dec_le, [| t1;t2 |])
- | Kapp(Lt, [t1;t2]) -> mkApp (Lazy.force coq_dec_lt, [| t1;t2 |])
- | Kapp(Ge, [t1;t2]) -> mkApp (Lazy.force coq_dec_ge, [| t1;t2 |])
- | Kapp(Gt, [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |])
+ | Kapp(op,[t1;t2]) ->
+ (try mkApp (Lazy.force (dec_binop op), [| t1; t2 |])
+ with Not_found -> raise Undecidable)
| Kapp(False,[]) -> Lazy.force coq_dec_False
| Kapp(True,[]) -> Lazy.force coq_dec_True
- | Kapp(Other t,_::_) -> error
- ("Omega: Unrecognized predicate or connective: "^t)
- | Kapp(Other t,[]) -> error ("Omega: Unrecognized atomic proposition: "^t)
- | Kvar _ -> error "Omega: Can't solve a goal with proposition variables"
- | _ -> error "Omega: Unrecognized proposition"
+ | _ -> raise Undecidable
let onClearedName id tac =
(* We cannot ensure that hyps can be cleared (because of dependencies), *)
@@ -1598,6 +1637,14 @@ let onClearedName id tac =
let id = fresh_id [] id gl in
tclTHEN (introduction id) (tac id) gl)
+let onClearedName2 id tac =
+ tclTHEN
+ (tclTRY (clear [id]))
+ (fun gl ->
+ let id1 = fresh_id [] (add_suffix id "_left") gl in
+ let id2 = fresh_id [] (add_suffix id "_right") gl in
+ tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] gl)
+
let destructure_hyps gl =
let rec loop = function
| [] -> (tclTHEN nat_inject coq_omega)
@@ -1611,50 +1658,24 @@ let destructure_hyps gl =
[ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
| Kapp(And,[t1;t2]) ->
- tclTHENLIST [
- (elim_id i);
- (tclTRY (clear [i]));
- (fun gl ->
- let i1 = fresh_id [] (add_suffix i "_left") gl in
- let i2 = fresh_id [] (add_suffix i "_right") gl in
- tclTHENLIST [
- (introduction i1);
- (introduction i2);
- (loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
- ]
+ tclTHEN
+ (elim_id i)
+ (onClearedName2 i (fun i1 i2 ->
+ loop ((i1,None,t1)::(i2,None,t2)::lit)))
| Kapp(Iff,[t1;t2]) ->
- tclTHENLIST [
- (elim_id i);
- (tclTRY (clear [i]));
- (fun gl ->
- let i1 = fresh_id [] (add_suffix i "_left") gl in
- let i2 = fresh_id [] (add_suffix i "_right") gl in
- tclTHENLIST [
- introduction i1;
- generalize_tac
- [mkApp (Lazy.force coq_imp_simp,
- [| t1; t2; decidability gl t1; mkVar i1|])];
- onClearedName i1 (fun i1 ->
- tclTHENLIST [
- introduction i2;
- generalize_tac
- [mkApp (Lazy.force coq_imp_simp,
- [| t2; t1; decidability gl t2; mkVar i2|])];
- onClearedName i2 (fun i2 ->
- loop
- ((i1,None,mk_or (mk_not t1) t2)::
- (i2,None,mk_or (mk_not t2) t1)::lit))
- ])] gl)
- ]
+ tclTHEN
+ (elim_id i)
+ (onClearedName2 i (fun i1 i2 ->
+ loop ((i1,None,mkArrow t1 t2)::(i2,None,mkArrow t2 t1)::lit)))
| Kimp(t1,t2) ->
- if
- is_Prop (pf_type_of gl t1) &
- is_Prop (pf_type_of gl t2) &
- closed0 t2
+ (* t1 and t2 might be in Type rather than Prop.
+ For t1, the decidability check will ensure being Prop. *)
+ if is_Prop (pf_type_of gl t2)
then
+ let d1 = decidability gl t1 in
tclTHENLIST [
(generalize_tac [mkApp (Lazy.force coq_imp_simp,
- [| t1; t2; decidability gl t1; mkVar i|])]);
+ [| t1; t2; d1; mkVar i|])]);
(onClearedName i (fun i ->
(loop ((i,None,mk_or (mk_not t1) t2)::lit))))
]
@@ -1670,86 +1691,53 @@ let destructure_hyps gl =
(loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
]
| Kapp(And,[t1;t2]) ->
+ let d1 = decidability gl t1 in
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_and, [| t1; t2;
- decidability gl t1; mkVar i|])]);
+ [mkApp (Lazy.force coq_not_and,
+ [| t1; t2; d1; mkVar i |])]);
(onClearedName i (fun i ->
(loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
]
| Kapp(Iff,[t1;t2]) ->
+ let d1 = decidability gl t1 in
+ let d2 = decidability gl t2 in
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_iff, [| t1; t2;
- decidability gl t1; decidability gl t2; mkVar i|])]);
+ [mkApp (Lazy.force coq_not_iff,
+ [| t1; t2; d1; d2; mkVar i |])]);
(onClearedName i (fun i ->
(loop ((i,None,
mk_or (mk_and t1 (mk_not t2))
(mk_and (mk_not t1) t2))::lit))))
]
| Kimp(t1,t2) ->
+ (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
+ For t1, being decidable implies being Prop. *)
+ let d1 = decidability gl t1 in
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_imp, [| t1; t2;
- decidability gl t1;mkVar i |])]);
+ [mkApp (Lazy.force coq_not_imp,
+ [| t1; t2; d1; mkVar i |])]);
(onClearedName i (fun i ->
(loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
]
| Kapp(Not,[t]) ->
+ let d = decidability gl t in
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_not, [| t;
- decidability gl t; mkVar i |])]);
+ [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
(onClearedName i (fun i -> (loop ((i,None,t)::lit))))
]
- | Kapp(Zle, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_Znot_le_gt, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Zge, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_Znot_ge_lt, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Zlt, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Zgt, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_Znot_gt_le, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Le, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_le, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Ge, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_ge, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Lt, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_lt, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Gt, [t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_gt, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
+ | Kapp(op,[t1;t2]) ->
+ (try
+ let thm = not_binop op in
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ with Not_found -> loop lit)
| Kapp(Eq,[typ;t1;t2]) ->
if !old_style_flag then begin
match destructurate_type (pf_nf gl typ) with
@@ -1787,7 +1775,9 @@ let destructure_hyps gl =
| _ -> loop lit
end
| _ -> loop lit
- with e when catchable_exception e -> loop lit
+ with
+ | Undecidable -> loop lit
+ | e when catchable_exception e -> loop lit
end
in
loop (pf_hyps gl) gl
@@ -1803,13 +1793,16 @@ let destructure_goal gl =
| Kimp(a,b) -> (tclTHEN intro (loop b))
| Kapp(False,[]) -> destructure_hyps
| _ ->
- (tclTHEN
- (tclTHEN
- (Tactics.refine
- (mkApp (Lazy.force coq_dec_not_not, [| t;
- decidability gl t; mkNewMeta () |])))
- intro)
- (destructure_hyps))
+ let goal_tac =
+ try
+ let dec = decidability gl t in
+ tclTHEN
+ (Tactics.refine
+ (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))
+ intro
+ with Undecidable -> Tactics.elim_type (build_coq_False ())
+ in
+ tclTHEN goal_tac destructure_hyps
in
(loop concl) gl
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index cd6472c3..84cc8464 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* 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 *)
@@ -15,8 +15,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_omega.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Coq_omega
open Refiner
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 8bb10194..3a5aece7 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* 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 *)
@@ -214,7 +214,7 @@ let rec display_action print_var = function
constant factors.\n" e1.id e2.id
| NEGATE_CONTRADICT(e1,e2,b) ->
Printf.printf
- "Equations E%d and E%d state that their body is at the same time
+ "Equations E%d and E%d state that their body is at the same time \
equal and different\n" e1.id e2.id
| CONSTANT_NOT_NUL (e,k) ->
Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 16:31:57 +0000