From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- plugins/omega/Omega.v | 4 +- plugins/omega/OmegaLemmas.v | 9 +- plugins/omega/OmegaPlugin.v | 4 +- plugins/omega/PreOmega.v | 115 +++++--------- plugins/omega/coq_omega.ml | 357 ++++++++++++++++++++++---------------------- plugins/omega/g_omega.ml4 | 4 +- plugins/omega/omega.ml | 4 +- 7 files changed, 227 insertions(+), 270 deletions(-) (limited to 'plugins/omega') 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 *) -(* 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 *) -(* 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 change (a change (a change (a change (a 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 generalize (Z_of_N_lt _ _ H); clear H; intro H - | |- (?a apply (Z_of_N_lt_rev a b) - | H : context [ (?a rewrite (Z_of_N_lt_iff a b) in H - | |- context [ (?a 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 *) -(* 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 *) -(* 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) -- cgit v1.2.3