diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/Fourier_util.v | 2 | ||||
| -rw-r--r-- | plugins/micromega/Lia.v | 4 | ||||
| -rw-r--r-- | plugins/micromega/RMicromega.v | 2 | ||||
| -rw-r--r-- | plugins/micromega/ZMicromega.v | 118 | ||||
| -rw-r--r-- | plugins/micromega/Zify.v | 2 | ||||
| -rw-r--r-- | plugins/micromega/ZifyBool.v | 29 | ||||
| -rw-r--r-- | plugins/micromega/ZifyComparison.v | 81 | ||||
| -rw-r--r-- | plugins/micromega/ZifyInst.v | 30 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 11 | ||||
| -rw-r--r-- | plugins/micromega/g_zify.mlg | 4 | ||||
| -rw-r--r-- | plugins/micromega/mutils.ml | 11 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 920 | ||||
| -rw-r--r-- | plugins/micromega/zify.mli | 1 |
13 files changed, 702 insertions, 513 deletions
diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v index b62153dee4..95fa5b88df 100644 --- a/plugins/micromega/Fourier_util.v +++ b/plugins/micromega/Fourier_util.v @@ -1,7 +1,7 @@ Require Export Rbase. Require Import Lra. -Open Scope R_scope. +Local Open Scope R_scope. Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. intros x y H H0; try assumption. diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 7e04fe0220..3351c7ef8a 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -44,9 +44,9 @@ Ltac zchecker_ext := (@eq_refl bool true <: @eq bool (ZTautoCheckerExt __ff __wit) true) (@find Z Z0 __varmap)). -Ltac lia := zify; xlia zchecker_ext. +Ltac lia := PreOmega.zify; xlia zchecker_ext. -Ltac nia := zify; xnlia zchecker. +Ltac nia := PreOmega.zify; xnlia zchecker. (* Local Variables: *) diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index d8282a1127..3651b54ed8 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -41,7 +41,7 @@ Proof. exact Rplus_opp_r. Qed. -Open Scope R_scope. +Local Open Scope R_scope. Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt. Proof. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 47c77ea927..c160e11467 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -22,8 +22,9 @@ Require FSetPositive FSetEqProperties. Require Import ZCoeff. Require Import Refl. Require Import ZArith. +Require PreOmega. (*Declare ML Module "micromega_plugin".*) -Open Scope Z_scope. +Local Open Scope Z_scope. Ltac flatten_bool := repeat match goal with @@ -100,11 +101,16 @@ Require Import EnvRing. Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt. Proof. - constructor ; intros ; subst ; try (intuition (auto with zarith)). + constructor ; intros ; subst; try reflexivity. apply Zsth. apply Zth. + auto using Z.le_antisymm. + eauto using Z.le_trans. + apply Z.le_neq. destruct (Z.lt_trichotomy n m) ; intuition. + apply Z.add_le_mono_l; assumption. apply Z.mul_pos_pos ; auto. + discriminate. Qed. Lemma ZSORaddon : @@ -195,7 +201,8 @@ Proof. (fun x : N => x) (pow_N 1 Z.mul) env Flhs). generalize ((eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env Frhs)). - destruct Fop ; simpl; intros ; intuition (auto with zarith). + destruct Fop ; simpl; intros; + intuition auto using Z.le_ge, Z.ge_le, Z.lt_gt, Z.gt_lt. Qed. @@ -489,7 +496,7 @@ Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : boo (* To get a complete checker, the proof format has to be enriched *) Require Import Zdiv. -Open Scope Z_scope. +Local Open Scope Z_scope. Definition ceiling (a b:Z) : Z := let (q,r) := Z.div_eucl a b in @@ -531,7 +538,10 @@ Proof. apply Z.mul_le_mono_pos_l in H; auto with zarith. - assert (0 < Z.pos r) by easy. rewrite Z.add_1_r, Z.le_succ_l. - apply Z.mul_lt_mono_pos_l with a; auto with zarith. + apply Z.mul_lt_mono_pos_l with a. + auto using Z.gt_lt. + eapply Z.lt_le_trans. 2: eassumption. + now apply Z.lt_add_pos_r. - now elim H1. Qed. @@ -627,20 +637,15 @@ Qed. Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0. Proof. - induction p. - simpl. auto with zarith. - simpl. auto. + induction p. 1-2: easy. simpl. case_eq (Zgcd_pol p1). case_eq (Zgcd_pol p3). intros. simpl. unfold ZgcdM. - generalize (Z.gcd_nonneg z1 z2). - generalize (Zmax_spec (Z.gcd z1 z2) 1). - generalize (Z.gcd_nonneg (Z.max (Z.gcd z1 z2) 1) z). - generalize (Zmax_spec (Z.gcd (Z.max (Z.gcd z1 z2) 1) z) 1). - auto with zarith. + apply Z.le_ge; transitivity 1. easy. + apply Z.le_max_r. Qed. Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p. @@ -698,7 +703,7 @@ Proof. induction p. simpl. intros. inversion H. - constructor. replace (c - 0) with c in H1 ; auto with zarith. + constructor. rewrite Z.sub_0_r in *. assumption. intros. constructor. simpl in H. inversion H ; subst; clear H. @@ -735,7 +740,7 @@ Proof. destruct HH2. rewrite H2. apply Zdivide_pol_sub ; auto. - auto with zarith. + apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le. destruct HH2. rewrite H2. apply Zdivide_pol_one. unfold ZgcdM in HH1. unfold ZgcdM. @@ -1050,7 +1055,7 @@ Fixpoint bdepth (pf : ZArithProof) : nat := | DoneProof => O | RatProof _ p => S (bdepth p) | CutProof _ p => S (bdepth p) - | EnumProof _ _ l => S (List.fold_right (fun pf x => Max.max (bdepth pf) x) O l) + | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l) end. Require Import Wf_nat. @@ -1069,19 +1074,19 @@ Proof. unfold ltof. simpl. generalize ( (fold_right - (fun (pf : ZArithProof) (x : nat) => Max.max (bdepth pf) x) 0%nat l)). + (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat l)). intros. generalize (bdepth y) ; intros. - generalize (Max.max_l n0 n) (Max.max_r n0 n). - auto with zarith. + rewrite Nat.lt_succ_r. apply Nat.le_max_l. generalize (IHl a0 b y H). unfold ltof. simpl. - generalize ( (fold_right (fun (pf : ZArithProof) (x : nat) => Max.max (bdepth pf) x) 0%nat + generalize ( (fold_right (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat l)). intros. - generalize (Max.max_l (bdepth a) n) (Max.max_r (bdepth a) n). - auto with zarith. + eapply lt_le_trans. eassumption. + rewrite <- Nat.succ_le_mono. + apply Nat.le_max_r. Qed. @@ -1113,10 +1118,14 @@ Proof. intros. inv H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. - apply Zgcd_pol_correct_lt with (env:=env) in H1. - generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). - auto with zarith. - auto with zarith. + apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt. + apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. + apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). + apply Z.le_ge. + rewrite <- Z.sub_0_l. + apply Z.le_sub_le_add_r. + rewrite <- H1. + assumption. (* g <= 0 *) intros. inv H2. auto with zarith. Qed. @@ -1143,7 +1152,7 @@ Proof. case_eq (Z.gtb g 0). intros. rewrite <- Zgt_is_gt_bool in H. - rewrite Zgcd_pol_correct_lt with (1:= H1) in H2; auto with zarith. + rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). inv H3. @@ -1159,7 +1168,7 @@ Proof. apply Zeq_bool_eq in H0. subst. simpl. rewrite Z.add_0_r, Z.mul_eq_0 in H2. - intuition auto with zarith. + intuition subst; easy. rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. assert (HH := Zgcd_is_gcd g c). @@ -1168,14 +1177,15 @@ Proof. apply Zdivide_opp_r in H4. rewrite Zdivide_ceiling ; auto. apply Z.sub_move_0_r. - apply Z.div_unique_exact ; auto with zarith. + apply Z.div_unique_exact. now intros ->. + now rewrite Z.add_move_0_r in H2. intros. unfold nformula_of_cutting_plane. inv H3. change (eval_pol env (padd e' (Pc 0)) = 0). rewrite eval_pol_add. simpl. - auto with zarith. + now rewrite Z.add_0_r. (* NonEqual *) intros. inv H0. @@ -1184,7 +1194,7 @@ Proof. unfold nformula_of_cutting_plane. unfold eval_op1 in *. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). - simpl. auto with zarith. + simpl. now rewrite Z.add_0_r. (* Strict *) destruct p as [[e' z] op]. case_eq (makeCuttingPlane (PsubC Z.sub e 1)). @@ -1193,7 +1203,7 @@ Proof. apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). - auto with zarith. + now apply Z.lt_le_pred. (* NonStrict *) destruct p as [[e' z] op]. case_eq (makeCuttingPlane e). @@ -1220,13 +1230,14 @@ Proof. rewrite negb_true_iff in H. apply Zeq_bool_neq in H. change (eval_pol env p = 0) in H2. - rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith. + rewrite Zgcd_pol_correct_lt with (1:= H0) in H2. 2: auto using Z.gt_lt. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x. contradict H5. - apply Zis_gcd_gcd; auto with zarith. + apply Zis_gcd_gcd. apply Z.lt_le_incl, Z.gt_lt; assumption. constructor; auto with zarith. exists (-x). - rewrite Z.mul_opp_l, Z.mul_comm; auto with zarith. + rewrite Z.mul_opp_l, Z.mul_comm. + now apply Z.add_move_0_l. (**) destruct (makeCuttingPlane p); discriminate. discriminate. @@ -1321,11 +1332,13 @@ Proof. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR. unfold eval_op1 in HCutR. destruct op1 ; simpl in Hop1 ; try discriminate; - rewrite eval_pol_add in HCutR; simpl in HCutR; auto with zarith. + rewrite eval_pol_add in HCutR; simpl in HCutR. + rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity. + now apply Z.le_sub_le_add_r in HCutR. (**) apply is_pol_Z0_eval_pol with (env := env) in HZ0. - rewrite eval_pol_add in HZ0. - replace (eval_pol env p1) with (- eval_pol env p2) by omega. + rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0. + rewrite HZ0. apply eval_Psatz_sound with (env:=env) in Hf1 ; auto. apply cutting_plane_sound with (1:= Hf1) in HCutL. unfold nformula_of_cutting_plane in HCutL. @@ -1334,7 +1347,10 @@ Proof. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL. unfold eval_op1 in HCutL. rewrite eval_pol_add in HCutL. simpl in HCutL. - destruct op2 ; simpl in Hop2 ; try discriminate ; omega. + destruct op2 ; simpl in Hop2 ; try discriminate. + rewrite Z.add_move_r, Z.sub_0_l in HCutL. + now rewrite HCutL, Z.opp_involutive. + now rewrite <- Z.le_sub_le_add_l in HCutL. revert Hfix. match goal with | |- context[?F pf (-z1) z2 = true] => set (FF := F) @@ -1348,26 +1364,24 @@ Proof. generalize (-z1). clear z1. intro z1. revert z1 z2. induction pf;simpl ;intros. - generalize (Zgt_cases z1 z2). - destruct (Z.gtb z1 z2). - intros. - apply False_ind ; omega. - discriminate. + revert Hfix. + now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x. flatten_bool. - assert (HH:(x = z1 \/ z1 +1 <=x)%Z) by omega. - destruct HH. - subst. - exists a ; auto. - assert (z1 + 1 <= x <= z2)%Z by omega. - elim IHpf with (2:=H2) (3:= H4). - destruct H4. + destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. + 2: exists a; auto. + rewrite <- Z.le_succ_l in LT. + assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. + elim IHpf with (2:=H2) (3:= LE). intros. exists x0 ; split;tauto. intros until 1. apply H ; auto. unfold ltof in *. simpl in *. - zify. omega. + PreOmega.zify. + intuition subst. assumption. + eapply Z.lt_le_trans. eassumption. + apply Z.add_le_mono_r. assumption. (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False). diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v index 57d812b0fd..785a53fafa 100644 --- a/plugins/micromega/Zify.v +++ b/plugins/micromega/Zify.v @@ -87,4 +87,4 @@ Ltac applySpec S := (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_tac ; (iter_specs applySpec) ; zify_post_hook. +Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook. diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v index ec37c2003f..b94b74097b 100644 --- a/plugins/micromega/ZifyBool.v +++ b/plugins/micromega/ZifyBool.v @@ -8,8 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Bool ZArith. -Require Import ZifyClasses. -Open Scope Z_scope. +Require Import Zify ZifyClasses. +Local Open Scope Z_scope. (* Instances of [ZifyClasses] for dealing with boolean operators. Various encodings of boolean are possible. One objective is to have an encoding that is terse but also lia friendly. @@ -42,6 +42,16 @@ Instance Op_orb : BinOp orb := TBOpInj := ltac:(destruct n,m; reflexivity)}. Add BinOp Op_orb. +Instance Op_implb : BinOp implb := + { TBOp := fun x y => Z.max (1 - x) y; + TBOpInj := ltac:(destruct n,m; reflexivity) }. +Add BinOp Op_implb. + +Instance Op_xorb : BinOp xorb := + { TBOp := fun x y => Z.max (x - y) (y - x); + TBOpInj := ltac:(destruct n,m; reflexivity) }. +Add BinOp Op_xorb. + Instance Op_negb : UnOp negb := { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}. Add UnOp Op_negb. @@ -52,10 +62,11 @@ Add BinRel Op_eq_bool. Instance Op_true : CstOp true := { TCst := 1 ; TCstInj := eq_refl }. +Add CstOp Op_true. Instance Op_false : CstOp false := { TCst := 0 ; TCstInj := eq_refl }. - +Add CstOp Op_false. (** Comparisons are encoded using the predicates [isZero] and [isLeZero].*) @@ -222,19 +233,23 @@ Add BinOp Op_nat_ltb. (** Injected boolean operators *) -Lemma Z_eqb_ZSpec_ok : forall x, x <> isZero x. +Lemma Z_eqb_ZSpec_ok : forall x, 0 <= isZero x <= 1 /\ + (x = 0 <-> isZero x = 1). Proof. intros. unfold isZero. destruct (x =? 0) eqn:EQ. - apply Z.eqb_eq in EQ. - simpl. congruence. + simpl. intuition try congruence; + compute ; congruence. - apply Z.eqb_neq in EQ. - simpl. auto. + simpl. intuition try congruence; + compute ; congruence. Qed. + Instance Z_eqb_ZSpec : UnOpSpec isZero := - {| UPred := fun n r => n <> r ; USpec := Z_eqb_ZSpec_ok |}. + {| UPred := fun n r => 0 <= r <= 1 /\ (n = 0 <-> isZero n = 1) ; USpec := Z_eqb_ZSpec_ok |}. Add Spec Z_eqb_ZSpec. Lemma leZeroSpec_ok : forall x, x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0. diff --git a/plugins/micromega/ZifyComparison.v b/plugins/micromega/ZifyComparison.v new file mode 100644 index 0000000000..8a8b40ded8 --- /dev/null +++ b/plugins/micromega/ZifyComparison.v @@ -0,0 +1,81 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Bool ZArith. +Require Import ZifyClasses. +Local Open Scope Z_scope. + +(** [Z_of_comparison] is the injection function for comparison *) +Definition Z_of_comparison (c : comparison) : Z := + match c with + | Lt => -1 + | Eq => 0 + | Gt => 1 + end. + +Lemma Z_of_comparison_bound : forall x, -1 <= Z_of_comparison x <= 1. +Proof. + destruct x ; simpl; compute; intuition congruence. +Qed. + +Instance Inj_comparison_Z : InjTyp comparison Z := + { inj := Z_of_comparison ; pred :=(fun x => -1 <= x <= 1) ; cstr := Z_of_comparison_bound}. +Add InjTyp Inj_comparison_Z. + +Definition ZcompareZ (x y : Z) := + Z_of_comparison (Z.compare x y). + +Program Instance BinOp_Zcompare : BinOp Z.compare := + { TBOp := ZcompareZ }. +Add BinOp BinOp_Zcompare. + +Instance Op_eq_comparison : BinRel (@eq comparison) := + {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }. +Add BinRel Op_eq_comparison. + +Instance Op_Eq : CstOp Eq := + { TCst := 0 ; TCstInj := eq_refl }. +Add CstOp Op_Eq. + +Instance Op_Lt : CstOp Lt := + { TCst := -1 ; TCstInj := eq_refl }. +Add CstOp Op_Lt. + +Instance Op_Gt : CstOp Gt := + { TCst := 1 ; TCstInj := eq_refl }. +Add CstOp Op_Gt. + + +Lemma Zcompare_spec : forall x y, + (x = y -> ZcompareZ x y = 0) + /\ + (x > y -> ZcompareZ x y = 1) + /\ + (x < y -> ZcompareZ x y = -1). +Proof. + unfold ZcompareZ. + intros. + destruct (x ?= y) eqn:C; simpl. + - rewrite Z.compare_eq_iff in C. + intuition. + - rewrite Z.compare_lt_iff in C. + intuition. + - rewrite Z.compare_gt_iff in C. + intuition. +Qed. + +Instance ZcompareSpec : BinOpSpec ZcompareZ := + {| BPred := fun x y r => (x = y -> r = 0) + /\ + (x > y -> r = 1) + /\ + (x < y -> r = -1) + ; BSpec := Zcompare_spec|}. +Add Spec ZcompareSpec. diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index 1217e8a5f7..afd7101667 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -15,7 +15,7 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. Require Import ZifyClasses. Declare ML Module "zify_plugin". -Open Scope Z_scope. +Local Open Scope Z_scope. (** Propositional logic *) Instance PropAnd : PropOp and. @@ -119,6 +119,7 @@ Add UnOp Op_S. Instance Op_O : CstOp O := {| TCst := Z0 ; TCstInj := eq_refl (Z.of_nat 0) |}. +Add CstOp Op_O. Instance Op_Z_abs_nat : UnOp Z.abs_nat := { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }. @@ -409,13 +410,34 @@ Add UnOp Op_Z_to_nat. (** Specification of derived operators over Z *) +Lemma z_max_spec : forall n m, + n <= Z.max n m /\ m <= Z.max n m /\ (Z.max n m = n \/ Z.max n m = m). +Proof. + intros. + generalize (Z.le_max_l n m). + generalize (Z.le_max_r n m). + generalize (Z.max_spec_le n m). + intuition idtac. +Qed. + Instance ZmaxSpec : BinOpSpec Z.max := {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}. Add Spec ZmaxSpec. -Instance ZminSpec : BinOpSpec Z.min := - {| BPred := fun n m r : Z => n < m /\ r = n \/ m <= n /\ r = m ; - BSpec := Z.min_spec|}. +Lemma z_min_spec : forall n m, + Z.min n m <= n /\ Z.min n m <= m /\ (Z.min n m = n \/ Z.min n m = m). +Proof. + intros. + generalize (Z.le_min_l n m). + generalize (Z.le_min_r n m). + generalize (Z.min_spec_le n m). + intuition idtac. +Qed. + + +Program Instance ZminSpec : BinOpSpec Z.min := + {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ; + BSpec := Z.min_spec |}. Add Spec ZminSpec. Instance ZsgnSpec : UnOpSpec Z.sgn := diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 90c9f86b07..1772a3c333 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -782,7 +782,7 @@ struct (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) let eq_constr gl x y = let evd = gl.sigma in - match EConstr.eq_constr_universes gl.env evd x y with + match EConstr.eq_constr_universes_proj gl.env evd x y with | Some csts -> let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in begin @@ -806,15 +806,16 @@ struct ({vars=vars';gl=gl'}, CamlToCoq.positive n) let get_rank env v = - let evd = env.gl.sigma in + let gl = env.gl in let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if EConstr.eq_constr evd e v - then n - else _get_rank l (n+1) in + match eq_constr gl e v with + | Some _ -> n + | None -> _get_rank l (n+1) + in _get_rank env.vars 1 let elements env = env.vars diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 424a7d7c54..66f263c0b1 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -26,7 +26,7 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF | ["Add" "CstOp" constr(t) ] -> { Zify.CstOp.register t } | ["Add" "BinRel" constr(t) ] -> { Zify.BinRel.register t } | ["Add" "PropOp" constr(t) ] -> { Zify.PropOp.register t } -| ["Add" "PropUOp" constr(t) ] -> { Zify.PropOp.register t } +| ["Add" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } | ["Add" "Spec" constr(t) ] -> { Zify.Spec.register t } | ["Add" "BinOpSpec" constr(t) ] -> { Zify.Spec.register t } | ["Add" "UnOpSpec" constr(t) ] -> { Zify.Spec.register t } @@ -38,7 +38,7 @@ TACTIC EXTEND ITER END TACTIC EXTEND TRANS -| [ "zify_tac" ] -> { Zify.zify_tac } +| [ "zify_op" ] -> { Zify.zify_tac } | [ "saturate" ] -> { Zify.saturate } END diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 39905f8c52..cca66c0719 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -106,12 +106,15 @@ let extract_best red lt l = | Some(c,e), rst -> extractb c e [] rst -let rec find_some pred l = +let rec find_option pred l = match l with - | [] -> None + | [] -> raise Not_found | e::l -> match pred e with - | Some r -> Some r - | None -> find_some pred l + | Some r -> r + | None -> find_option pred l + +let find_some pred l = + try Some (find_option pred l) with Not_found -> None let extract_all pred l = diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index be6037ccdb..0a57677220 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -24,27 +24,13 @@ let unsafe_to_constr = EConstr.Unsafe.to_constr let pr_constr env evd e = Printer.pr_econstr_env env evd e -(** [get_arrow_typ evd t] returns [t1;.tn] such that t = t1 -> .. -> tn.ci_npar - (only syntactic matching) - *) -let rec get_arrow_typ evd t = - match EConstr.kind evd t with - | Prod (a, p1, p2) (*when a.Context.binder_name = Names.Anonymous*) -> - p1 :: get_arrow_typ evd p2 - | _ -> [t] - -(** [get_binary_arrow t] return t' such that t = t' -> t' -> t' *) -let get_binary_arrow evd t = - let l = get_arrow_typ evd t in +let rec find_option pred l = match l with - | [] -> assert false - | [t1; t2; t3] -> Some (t1, t2, t3) - | _ -> None + | [] -> raise Not_found + | e::l -> match pred e with + | Some r -> r + | None -> find_option pred l -(** [get_unary_arrow t] return t' such that t = t' -> t' *) -let get_unary_arrow evd t = - let l = get_arrow_typ evd t in - match l with [] -> assert false | [t1; t2] -> Some (t1, t2) | _ -> None (** [HConstr] is a map indexed by EConstr.t. It should only be used using closed terms. @@ -57,6 +43,8 @@ module HConstr = struct Constr.compare (unsafe_to_constr c) (unsafe_to_constr c') end) + type 'a t = 'a list M.t + let lfind h m = try M.find h m with Not_found -> [] let add h e m = @@ -72,27 +60,23 @@ module HConstr = struct let fold f m acc = M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc - let iter = M.iter - end + (** [get_projections_from_constant (evd,c) ] returns an array of constr [| a1,.. an|] such that [c] is defined as Definition c := mk a1 .. an with mk a constructor. ai is therefore either a type parameter or a projection. *) -let get_projections_from_constant (evd, i) = - match Constr.kind (unsafe_to_constr i) with - | Constr.Const (c, u) -> - (match Environ.constant_opt_value_in (Global.env ()) (c,u) with - | None -> failwith "Add Injection requires a constant (with a body)" - | Some c -> ( - match EConstr.kind evd (EConstr.of_constr c) with - | App (c, a) -> Some a - | _ -> None )) - | _ -> None +let get_projections_from_constant (evd, i) = + match EConstr.kind evd (Reductionops.clos_whd_flags CClosure.all (Global.env ()) evd i) with + | App (c, a) -> Some a + | _ -> + raise (CErrors.user_err Pp.(str "The hnf of term " ++ pr_constr (Global.env ()) evd i + ++ str " should be an application i.e. (c a1 ... an)")) + (** An instance of type, say T, is registered into a hashtable, say TableT. *) type 'a decl = @@ -101,34 +85,111 @@ type 'a decl = deriv: 'a (* Projections of insterest *) } -(* Different type of declarations *) -type decl_kind = - | PropOp - | InjTyp - | BinRel - | BinOp - | UnOp - | CstOp - | Saturate -let string_of_decl = function - | PropOp -> "PropOp" - | InjTyp -> "InjTyp" - | BinRel -> "BinRel" - | BinOp -> "BinOp" - | UnOp -> "UnOp" - | CstOp -> "CstOp" - | Saturate -> "Saturate" +module EInjT = struct + type t = + { isid: bool + ; (* S = T -> inj = fun x -> x*) + source: EConstr.t + ; (* S *) + target: EConstr.t + ; (* T *) + (* projections *) + inj: EConstr.t + ; (* S -> T *) + pred: EConstr.t + ; (* T -> Prop *) + cstr: EConstr.t option + (* forall x, pred (inj x) *) } +end +module EBinOpT = struct + type t = + { (* Op : source1 -> source2 -> source3 *) + source1: EConstr.t + ; source2: EConstr.t + ; source3: EConstr.t + ; target: EConstr.t + ; inj1: EConstr.t + ; (* InjTyp source1 target *) + inj2: EConstr.t + ; (* InjTyp source2 target *) + inj3: EConstr.t + ; (* InjTyp source3 target *) + tbop: EConstr.t + (* TBOpInj *) } +end +module ECstOpT = struct + type t = {source: EConstr.t; target: EConstr.t; inj: EConstr.t} +end +module EUnOpT = struct + type t = + { source1: EConstr.t + ; source2: EConstr.t + ; target: EConstr.t + ; inj1_t: EConstr.t + ; inj2_t: EConstr.t + ; unop: EConstr.t } +end + +module EBinRelT = struct + type t = + {source: EConstr.t; target: EConstr.t; inj: EConstr.t; brel: EConstr.t} +end + +module EPropBinOpT = struct + type t = EConstr.t +end + +module EPropUnOpT = struct + type t = EConstr.t +end + + +module ESatT = struct + type t = {parg1: EConstr.t; parg2: EConstr.t; satOK: EConstr.t} +end + +(* Different type of declarations *) +type decl_kind = + | PropOp of EPropBinOpT.t decl + | PropUnOp of EPropUnOpT.t decl + | InjTyp of EInjT.t decl + | BinRel of EBinRelT.t decl + | BinOp of EBinOpT.t decl + | UnOp of EUnOpT.t decl + | CstOp of ECstOpT.t decl + | Saturate of ESatT.t decl + + +let get_decl = function + | PropOp d -> d.decl + | PropUnOp d -> d.decl + | InjTyp d -> d.decl + | BinRel d -> d.decl + | BinOp d -> d.decl + | UnOp d -> d.decl + | CstOp d -> d.decl + | Saturate d -> d.decl + +type term_kind = + | Application of EConstr.constr + | OtherTerm of EConstr.constr module type Elt = sig type elt - val name : decl_kind - (** [name] of the table *) + val name : string + (** name *) + + val table : (term_kind * decl_kind) HConstr.t ref + + val cast : elt decl -> decl_kind + + val dest : decl_kind -> (elt decl) option val get_key : int (** [get_key] is the type-index used as key for the instance *) @@ -138,128 +199,36 @@ module type Elt = sig built from the type-instance i and the arguments (type indexes and projections) of the type-class constructor. *) - val reduce_term : Evd.evar_map -> EConstr.t -> EConstr.t - (** [reduce_term evd t] normalises [t] in a table dependent way. *) - -end - -module type S = sig - val register : Constrexpr.constr_expr -> unit + (* val arity : int*) - val print : unit -> unit end -let not_registered = Summary.ref ~name:"zify_to_register" [] - -module MakeTable (E : Elt) = struct - (** Given a term [c] and its arguments ai, - we construct a HConstr.t table that is - indexed by ai for i = E.get_key. - The elements of the table are built using E.mk_elt c [|a0,..,an|] - *) - - let make_elt (evd, i) = - match get_projections_from_constant (evd, i) with - | None -> - let env = Global.env () in - let t = string_of_ppcmds (pr_constr env evd i) in - failwith ("Cannot register term " ^ t) - | Some a -> E.mk_elt evd i a - let table = Summary.ref ~name:("zify_" ^ string_of_decl E.name) HConstr.empty +let table = Summary.ref ~name:("zify_table") HConstr.empty - let register_constr env evd c = - let c = EConstr.of_constr c in - let t = get_type_of env evd c in - match EConstr.kind evd t with - | App (intyp, args) -> - let styp = E.reduce_term evd args.(E.get_key) in - let elt = {decl= c; deriv= make_elt (evd, c)} in - table := HConstr.add styp elt !table - | _ -> failwith "Can only register terms of type [F X1 .. Xn]" +let saturate = Summary.ref ~name:("zify_saturate") HConstr.empty - let get evd c = - let c' = E.reduce_term evd c in - HConstr.find c' !table +let table_cache = ref HConstr.empty +let saturate_cache = ref HConstr.empty - let get_all evd c = - let c' = E.reduce_term evd c in - HConstr.find_all c' !table - let fold_declared_const f evd acc = - HConstr.fold - (fun _ e acc -> f (fst (EConstr.destConst evd e.decl)) acc) - !table acc +(** Each type-class gives rise to a different table. + They only differ on how projections are extracted. *) +module EInj = struct + open EInjT - exception FoundNorm of EConstr.t + type elt = EInjT.t - let can_unify evd k t = - try - let _ = Unification.w_unify (Global.env ()) evd Reduction.CONV k t in - true ; - with _ -> false + let name = "EInj" - let unify_with_key evd t = - try - HConstr.iter - (fun k _ -> - if can_unify evd k t - then raise (FoundNorm k) - else ()) !table ; t - with FoundNorm k -> k + let table = table + let cast x = InjTyp x - let pp_keys () = - let env = Global.env () in - let evd = Evd.from_env env in - HConstr.fold - (fun k _ acc -> Pp.(pr_constr env evd k ++ str " " ++ acc)) - !table (Pp.str "") + let dest = function + | InjTyp x -> Some x + | _ -> None - let register_obj : Constr.constr -> Libobject.obj = - let cache_constr (_, c) = - not_registered := (E.name,c)::!not_registered - in - let subst_constr (subst, c) = Mod_subst.subst_mps subst c in - Libobject.declare_object - @@ Libobject.superglobal_object_nodischarge - ("register-zify-" ^ string_of_decl E.name) - ~cache:cache_constr ~subst:(Some subst_constr) - - (** [register c] is called from the VERNACULAR ADD [name] constr(t). - The term [c] is interpreted and - registered as a [superglobal_object_nodischarge]. - TODO: pre-compute [get_type_of] - [cache_constr] is using another environment. - *) - let register c = - let env = Global.env () in - let evd = Evd.from_env env in - let evd, c = Constrintern.interp_open_constr env evd c in - let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in - () - - let print () = Feedback.msg_notice (pp_keys ()) -end - -(** Each type-class gives rise to a different table. - They only differ on how projections are extracted. *) -module InjElt = struct - type elt = - { isid: bool - ; (* S = T -> inj = fun x -> x*) - source: EConstr.t - ; (* S *) - target: EConstr.t - ; (* T *) - (* projections *) - inj: EConstr.t - ; (* S -> T *) - pred: EConstr.t - ; (* T -> Prop *) - cstr: EConstr.t option - (* forall x, pred (inj x) *) } - - let name = InjTyp let mk_elt evd i (a : EConstr.t array) = let isid = EConstr.eq_constr evd a.(0) a.(1) in @@ -272,40 +241,15 @@ module InjElt = struct let get_key = 0 - let reduce_term evd t = t - end -module InjTable = MakeTable (InjElt) - - -let coq_eq = lazy ( EConstr.of_constr - (UnivGen.constr_of_monomorphic_global - (Coqlib.lib_ref ("core.eq.type")))) - -let reduce_type evd ty = - try ignore (InjTable.get evd ty) ; ty - with Not_found -> - (* Maybe it unifies *) - InjTable.unify_with_key evd ty - module EBinOp = struct - type elt = - { (* Op : source1 -> source2 -> source3 *) - source1: EConstr.t - ; source2: EConstr.t - ; source3: EConstr.t - ; target: EConstr.t - ; inj1: EConstr.t - ; (* InjTyp source1 target *) - inj2: EConstr.t - ; (* InjTyp source2 target *) - inj3: EConstr.t - ; (* InjTyp source3 target *) - tbop: EConstr.t - (* TBOpInj *) } + type elt = EBinOpT.t + open EBinOpT + + let name = "BinOp" - let name = BinOp + let table = table let mk_elt evd i a = { source1= a.(0) @@ -319,34 +263,50 @@ module EBinOp = struct let get_key = 4 - let reduce_term evd t = t + + let cast x = BinOp x + + let dest = function + | BinOp x -> Some x + | _ -> None end module ECstOp = struct - type elt = {source: EConstr.t; target: EConstr.t; inj: EConstr.t} + type elt = ECstOpT.t + open ECstOpT + + let name = "CstOp" + + let table = table + + let cast x = CstOp x + + let dest = function + | CstOp x -> Some x + | _ -> None - let name = CstOp let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3)} let get_key = 2 - let reduce_term evd t = t - end - module EUnOp = struct - type elt = - { source1: EConstr.t - ; source2: EConstr.t - ; target: EConstr.t - ; inj1_t: EConstr.t - ; inj2_t: EConstr.t - ; unop: EConstr.t } + type elt = EUnOpT.t + open EUnOpT + + let name = "UnOp" + + let table = table + + let cast x = UnOp x + + let dest = function + | UnOp x -> Some x + | _ -> None - let name = UnOp let mk_elt evd i a = { source1= a.(0) @@ -358,72 +318,202 @@ module EUnOp = struct let get_key = 3 - let reduce_term evd t = t - end -open EUnOp - module EBinRel = struct - type elt = - {source: EConstr.t; target: EConstr.t; inj: EConstr.t; brel: EConstr.t} + type elt = EBinRelT.t + open EBinRelT + + let name = "BinRel" + + let table = table + + let cast x = BinRel x - let name = BinRel + let dest = function + | BinRel x -> Some x + | _ -> None let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3); brel= a.(4)} let get_key = 2 +end + +module EPropOp = struct + type elt = EConstr.t + + let name = "PropBinOp" - (** [reduce_term evd t] if t = @eq ty normalises ty to a declared type e.g Z if it exists. *) - let reduce_term evd t = - match EConstr.kind evd t with - | App(c,a) -> if EConstr.eq_constr evd (Lazy.force coq_eq) c - then - match a with - | [| ty |] -> EConstr.mkApp(c,[| reduce_type evd ty|]) - | _ -> t - else t - | _ -> t + let table = table + + let cast x = PropOp x + + let dest = function + | PropOp x -> Some x + | _ -> None + + let mk_elt evd i a = i + + let get_key = 0 end -module EPropOp = struct +module EPropUnOp = struct type elt = EConstr.t - let name = PropOp + let name = "PropUnOp" + + let table = table + + let cast x = PropUnOp x + + let dest = function + | PropUnOp x -> Some x + | _ -> None let mk_elt evd i a = i let get_key = 0 - let reduce_term evd t = t +end + + + +let constr_of_term_kind = function + | Application c -> c + | OtherTerm c -> c + + +let fold_declared_const f evd acc = + HConstr.fold + (fun _ (_,e) acc -> f (fst (EConstr.destConst evd (get_decl e))) acc) + (!table_cache) acc + + + +module type S = sig + val register : Constrexpr.constr_expr -> unit + + val print : unit -> unit end -module ESat = struct - type elt = {parg1: EConstr.t; parg2: EConstr.t; satOK: EConstr.t} - let name = Saturate +module MakeTable (E : Elt) = struct + (** Given a term [c] and its arguments ai, + we construct a HConstr.t table that is + indexed by ai for i = E.get_key. + The elements of the table are built using E.mk_elt c [|a0,..,an|] + *) - let mk_elt evd i a = {parg1= a.(2); parg2= a.(3); satOK= a.(5)} + let make_elt (evd, i) = + match get_projections_from_constant (evd, i) with + | None -> + let env = Global.env () in + let t = string_of_ppcmds (pr_constr env evd i) in + failwith ("Cannot register term " ^ t) + | Some a -> E.mk_elt evd i a + + let register_hint evd t elt = + match EConstr.kind evd t with + | App(c,_) -> + E.table := HConstr.add c (Application t, E.cast elt) !E.table + | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table - let get_key = 1 - let reduce_term evd t = t + + + let register_constr env evd c = + let c = EConstr.of_constr c in + let t = get_type_of env evd c in + match EConstr.kind evd t with + | App (intyp, args) -> + let styp = args.(E.get_key) in + let elt = {decl= c; deriv= (make_elt (evd, c))} in + register_hint evd styp elt + | _ -> + let env = Global.env () in + raise (CErrors.user_err Pp. + (str ": Cannot register term "++pr_constr env evd c++ + str ". It has type "++pr_constr env evd t++str " which should be of the form [F X1 .. Xn]")) + + let register_obj : Constr.constr -> Libobject.obj = + let cache_constr (_, c) = + let env = Global.env () in + let evd = Evd.from_env env in + register_constr env evd c + in + let subst_constr (subst, c) = Mod_subst.subst_mps subst c in + Libobject.declare_object + @@ Libobject.superglobal_object_nodischarge + ("register-zify-" ^ E.name) + ~cache:cache_constr ~subst:(Some subst_constr) + + (** [register c] is called from the VERNACULAR ADD [name] constr(t). + The term [c] is interpreted and + registered as a [superglobal_object_nodischarge]. + TODO: pre-compute [get_type_of] - [cache_constr] is using another environment. + *) + let register = fun c -> + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c = Constrintern.interp_open_constr env evd c in + let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in + () + + + let pp_keys () = + let env = Global.env () in + let evd = Evd.from_env env in + HConstr.fold + (fun _ (k,d) acc -> + match E.dest d with + | None -> acc + | Some _ -> + Pp.(pr_constr env evd (constr_of_term_kind k) ++ str " " ++ acc)) + (!E.table) (Pp.str "") + + + let print () = Feedback.msg_info (pp_keys ()) end +module InjTable = MakeTable (EInj) + + +module ESat = struct + type elt = ESatT.t + open ESatT + + let name = "Saturate" + + let table = saturate + + let cast x = Saturate x + + let dest = function + | Saturate x -> Some x + | _ -> None + + let mk_elt evd i a = {parg1= a.(2); parg2= a.(3); satOK= a.(5)} + + let get_key = 1 + +end module BinOp = MakeTable (EBinOp) module UnOp = MakeTable (EUnOp) module CstOp = MakeTable (ECstOp) module BinRel = MakeTable (EBinRel) module PropOp = MakeTable (EPropOp) +module PropUnOp = MakeTable (EPropUnOp) module Saturate = MakeTable (ESat) - +let init_cache () = + table_cache := !table; + saturate_cache := !saturate (** The module [Spec] is used to register @@ -467,37 +557,11 @@ module Spec = struct end -let register_decl = function - | PropOp -> PropOp.register_constr - | InjTyp -> InjTable.register_constr - | BinRel -> BinRel.register_constr - | BinOp -> BinOp.register_constr - | UnOp -> UnOp.register_constr - | CstOp -> CstOp.register_constr - | Saturate -> Saturate.register_constr - - -let process_decl (d,c) = - let env = Global.env () in - let evd = Evd.from_env env in - register_decl d env evd c - -let process_all_decl () = - List.iter process_decl !not_registered ; - not_registered := [] - - let unfold_decl evd = let f cst acc = cst :: acc in - let acc = InjTable.fold_declared_const f evd [] in - let acc = BinOp.fold_declared_const f evd acc in - let acc = UnOp.fold_declared_const f evd acc in - let acc = CstOp.fold_declared_const f evd acc in - let acc = BinRel.fold_declared_const f evd acc in - let acc = PropOp.fold_declared_const f evd acc in - acc + fold_declared_const f evd [] -open InjElt +open EInjT (** Get constr of lemma and projections in ZifyClasses. *) @@ -545,7 +609,7 @@ let iff = lazy (zify "iff") let to_unfold = lazy - (List.map locate_const + (List.rev_map locate_const [ "source_prop" ; "target_prop" ; "uop_iff" @@ -567,6 +631,7 @@ let to_unfold = ; "mkapp0" ; "mkprop_op" ]) + (** Module [CstrTable] records terms [x] injected into [inj x] together with the corresponding type constraint. The terms are stored by side-effect during the traversal @@ -585,7 +650,7 @@ module CstrTable = struct let table : EConstr.t HConstr.t = HConstr.create 10 - let register evd t (i : EConstr.t) = HConstr.replace table t i + let register evd t (i : EConstr.t) = HConstr.add table t i let get () = let l = HConstr.fold (fun k i acc -> (k, i) :: acc) table [] in @@ -601,7 +666,7 @@ module CstrTable = struct let has_hyp = let hyps_table = HConstr.create 20 in List.iter - (fun (_, (t : EConstr.types)) -> HConstr.replace hyps_table t ()) + (fun (_, (t : EConstr.types)) -> HConstr.add hyps_table t ()) (Tacmach.New.pf_hyps_types gl) ; fun c -> HConstr.mem hyps_table c in @@ -641,9 +706,9 @@ let mkvar red evd inj v = ; EConstr.mkApp (force eq_refl, [|inj.target; iv|]) |] ) type texpr = - | Var of InjElt.elt * EConstr.t + | Var of EInj.elt * EConstr.t (** Var is a term that cannot be injected further *) - | Constant of InjElt.elt * EConstr.t + | Constant of EInj.elt * EConstr.t (** Constant is a term that is solely built from constructors *) | Injterm of EConstr.t (** Injected is an injected term represented by a term of type [injterm] *) @@ -667,7 +732,7 @@ let mkapp2_id evd i (* InjTyp S3 T *) let default () = let e1' = inj_term_of_texpr evd e1 in let e2' = inj_term_of_texpr evd e2 in - EBinOp.( + EBinOpT.( Injterm (EConstr.mkApp ( force mkapp2 @@ -694,7 +759,7 @@ let mkapp2_id evd i (* InjTyp S3 T *) | _, _ -> default () let mkapp_id evd i inj (unop, u) f e1 = - if EConstr.eq_constr evd u.unop f then + EUnOpT.(if EConstr.eq_constr evd u.unop f then (* Injection does nothing *) match e1 with | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|])) @@ -716,61 +781,109 @@ let mkapp_id evd i inj (unop, u) f e1 = (EConstr.mkApp ( force mkapp , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|] - )) + ))) type typed_constr = {constr: EConstr.t; typ: EConstr.t} -type op = - | Unop of - { unop: EConstr.t - ; (* unop : typ unop_arg -> unop_typ *) - unop_typ: EConstr.t - ; unop_arg: typed_constr } - | Binop of - { binop: EConstr.t - ; (* binop : typ binop_arg1 -> typ binop_arg2 -> binop_typ *) - binop_typ: EConstr.t - ; binop_arg1: typed_constr - ; binop_arg2: typed_constr } - - -let rec trans_expr env evd e = + + +let get_injection env evd t = + match snd (HConstr.find t !table_cache) with + | InjTyp i -> i + | _ -> raise Not_found + + + (* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *) + let arrow = + let name x = + Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant in + EConstr.mkLambda + ( name "x" + , EConstr.mkProp + , EConstr.mkLambda + ( name "y" + , EConstr.mkProp + , EConstr.mkProd + ( Context.make_annot Names.Anonymous Sorts.Relevant + , EConstr.mkRel 2 + , EConstr.mkRel 2 ) ) ) + + + let is_prop env sigma term = + let sort = Retyping.get_sort_of env sigma term in + Sorts.is_prop sort + + (** [get_application env evd e] expresses [e] as an application (c a) + where c is the head symbol and [a] is the array of arguments. + The function also transforms (x -> y) as (arrow x y) *) + let get_operator env evd e = + let is_arrow a p1 p2 = + is_prop env evd p1 && is_prop (EConstr.push_rel (Context.Rel.Declaration.LocalAssum(a,p1)) env) evd p2 + && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) in + match EConstr.kind evd e with + | Prod (a, p1, p2) when is_arrow a p1 p2 -> + (arrow,[|p1 ;p2|]) + | App(c,a) -> (c,a) + | _ -> (e,[||]) + + + let is_convertible env evd k t = + Reductionops.check_conv env evd k t + + (** [match_operator env evd hd arg (t,d)] + - hd is head operator of t + - If t = OtherTerm _, then t = hd + - If t = Application _, then + we extract the relevant number of arguments from arg + and check for convertibility *) + let match_operator env evd hd args (t, d) = + let decomp t i = + let n = Array.length args in + let t' = EConstr.mkApp(hd,Array.sub args 0 (n-i)) in + if is_convertible env evd t' t + then Some (d,t) + else None in + + match t with + | OtherTerm t -> Some(d,t) + | Application t -> + match d with + | CstOp _ -> decomp t 0 + | UnOp _ -> decomp t 1 + | BinOp _ -> decomp t 2 + | BinRel _ -> decomp t 2 + | PropOp _ -> decomp t 2 + | PropUnOp _ -> decomp t 1 + | _ -> None + + + let rec trans_expr env evd e = (* Get the injection *) - let {decl= i; deriv= inj} = InjTable.get evd e.typ in + let {decl= i; deriv= inj} = get_injection env evd e.typ in let e = e.constr in if EConstr.isConstruct evd e then Constant (inj, e) (* Evaluate later *) else + let (c,a) = get_operator env evd e in try - (* The term [e] might be a registered constant *) - let {decl= c} = CstOp.get evd e in - Injterm - (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c|])) - with Not_found -> ( - (* Let decompose the term *) - match EConstr.kind evd e with - | App (t, a) -> ( - try - match Array.length a with - | 1 -> - let {decl= unop; deriv= u} = UnOp.get evd t in - let a' = trans_expr env evd {constr= a.(0); typ= u.source1} in - if is_constant a' && EConstr.isConstruct evd t then - Constant (inj, e) - else mkapp_id evd i inj (unop, u) t a' - | 2 -> - let {decl= bop; deriv= b} = BinOp.get evd t in - let a0 = - trans_expr env evd {constr= a.(0); typ= b.EBinOp.source1} - in - let a1 = - trans_expr env evd {constr= a.(1); typ= b.EBinOp.source2} - in - if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t - then Constant (inj, e) - else mkapp2_id evd i inj t bop b a0 a1 - | _ -> Var (inj, e) - with Not_found -> Var (inj, e) ) - | _ -> Var (inj, e) ) + let (k,t) = find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) in + let n = Array.length a in + match k with + | CstOp {decl = c'} -> + Injterm (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c'|])) + | UnOp {decl = unop ; deriv = u} -> + let a' = trans_expr env evd {constr= a.(n-1); typ= u.EUnOpT.source1} in + if is_constant a' && EConstr.isConstruct evd t then + Constant (inj, e) + else mkapp_id evd i inj (unop, u) t a' + | BinOp {decl = binop ; deriv = b} -> + let a0 = trans_expr env evd {constr= a.(n-2); typ= b.EBinOpT.source1} in + let a1 = trans_expr env evd {constr= a.(n-1); typ= b.EBinOpT.source2} in + if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t + then Constant (inj, e) + else mkapp2_id evd i inj t binop b a0 a1 + | d -> + Var (inj,e) + with Not_found -> Var (inj,e) let trans_expr env evd e = try trans_expr env evd e with Not_found -> @@ -779,68 +892,6 @@ let trans_expr env evd e = ( Pp.str "Missing injection for type " ++ Printer.pr_leconstr_env env evd e.typ )) -let is_prop env sigma term = - let sort = Retyping.get_sort_of env sigma term in - Sorts.is_prop sort - -let get_rel env evd e = - let is_arrow a p1 p2 = - is_prop env evd p1 && is_prop (EConstr.push_rel (Context.Rel.Declaration.LocalAssum(a,p1)) env) evd p2 - && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) - in - match EConstr.kind evd e with - | Prod (a, p1, p2) when is_arrow a p1 p2 -> - (* X -> Y becomes (fun x y => x -> y) x y *) - let name x = - Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant - in - let arrow = - EConstr.mkLambda - ( name "x" - , EConstr.mkProp - , EConstr.mkLambda - ( name "y" - , EConstr.mkProp - , EConstr.mkProd - ( Context.make_annot Names.Anonymous Sorts.Relevant - , EConstr.mkRel 2 - , EConstr.mkRel 2 ) ) ) - in - Binop - { binop= arrow - ; binop_typ= EConstr.mkProp - ; binop_arg1= {constr= p1; typ= EConstr.mkProp} - ; binop_arg2= {constr= p2; typ= EConstr.mkProp} } - | App (c, a) -> - let len = Array.length a in - if len >= 2 then - let c, a1, a2 = - if len = 2 then (c, a.(0), a.(1)) - else if len > 2 then - ( EConstr.mkApp (c, Array.sub a 0 (len - 2)) - , a.(len - 2) - , a.(len - 1) ) - else raise Not_found - in - let typ = get_type_of env evd c in - match get_binary_arrow evd typ with - | None -> raise Not_found - | Some (t1, t2, t3) -> - Binop - { binop= c - ; binop_typ= t3 - ; binop_arg1= {constr= a1; typ= t1} - ; binop_arg2= {constr= a2; typ= t2} } - else if len = 1 then - let typ = get_type_of env evd c in - match get_unary_arrow evd typ with - | None -> raise Not_found - | Some (t1, t2) -> - Unop {unop= c; unop_typ= t2; unop_arg= {constr= a.(0); typ= t1}} - else raise Not_found - | _ -> raise Not_found - -let get_rel env evd e = try Some (get_rel env evd e) with Not_found -> None type tprop = | TProp of EConstr.t (** Transformed proposition *) @@ -852,47 +903,42 @@ let mk_iprop e = let inj_prop_of_tprop = function TProp p -> p | IProp e -> mk_iprop e let rec trans_prop env evd e = - match get_rel env evd e with - | None -> IProp e - | Some (Binop {binop= r; binop_typ= t1; binop_arg1= a1; binop_arg2= a2}) -> - assert (EConstr.eq_constr evd EConstr.mkProp t1) ; - if EConstr.eq_constr evd a1.typ a2.typ then - (* Arguments have the same type *) - if - EConstr.eq_constr evd EConstr.mkProp t1 - && EConstr.eq_constr evd EConstr.mkProp a1.typ - then - (* Prop -> Prop -> Prop *) - try - let {decl= rop} = PropOp.get evd r in - let t1 = trans_prop env evd a1.constr in - let t2 = trans_prop env evd a2.constr in - match (t1, t2) with + let (c,a) = get_operator env evd e in + try + let (k,t) = find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) in + let n = Array.length a in + match k with + | PropOp {decl= rop} -> + begin + try + let t1 = trans_prop env evd a.(n-2) in + let t2 = trans_prop env evd a.(n-1) in + match (t1, t2) with | IProp _, IProp _ -> IProp e | _, _ -> - let t1 = inj_prop_of_tprop t1 in + let t1 = inj_prop_of_tprop t1 in let t2 = inj_prop_of_tprop t2 in - TProp (EConstr.mkApp (force mkprop_op, [|r; rop; t1; t2|])) - with Not_found -> IProp e - else - (* A -> A -> Prop *) - try - let {decl= br; deriv= rop} = BinRel.get evd r in - let a1 = trans_expr env evd {a1 with typ = rop.EBinRel.source} in - let a2 = trans_expr env evd {a2 with typ = rop.EBinRel.source} in - if EConstr.eq_constr evd r rop.EBinRel.brel then + TProp (EConstr.mkApp (force mkprop_op, [|t; rop; t1; t2|])) + with Not_found -> IProp e + end + | BinRel {decl = br ; deriv = rop} -> + begin + try + let a1 = trans_expr env evd {constr = a.(n-2) ; typ = rop.EBinRelT.source} in + let a2 = trans_expr env evd {constr = a.(n-1) ; typ = rop.EBinRelT.source} in + if EConstr.eq_constr evd t rop.EBinRelT.brel then match (constr_of_texpr a1, constr_of_texpr a2) with - | Some e1, Some e2 -> IProp (EConstr.mkApp (r, [|e1; e2|])) + | Some e1, Some e2 -> IProp (EConstr.mkApp (t, [|e1; e2|])) | _, _ -> let a1 = inj_term_of_texpr evd a1 in let a2 = inj_term_of_texpr evd a2 in TProp (EConstr.mkApp ( force mkrel - , [| rop.EBinRel.source - ; rop.EBinRel.target - ; r - ; rop.EBinRel.inj + , [| rop.EBinRelT.source + ; rop.EBinRelT.target + ; t + ; rop.EBinRelT.inj ; br ; a1 ; a2 |] )) @@ -902,37 +948,35 @@ let rec trans_prop env evd e = TProp (EConstr.mkApp ( force mkrel - , [| rop.EBinRel.source - ; rop.EBinRel.target - ; r - ; rop.EBinRel.inj + , [| rop.EBinRelT.source + ; rop.EBinRelT.target + ; t + ; rop.EBinRelT.inj ; br ; a1 ; a2 |] )) with Not_found -> IProp e - else IProp e - | Some (Unop {unop; unop_typ; unop_arg}) -> - if - EConstr.eq_constr evd EConstr.mkProp unop_typ - && EConstr.eq_constr evd EConstr.mkProp unop_arg.typ - then - try - let {decl= rop} = PropOp.get evd unop in - let t1 = trans_prop env evd unop_arg.constr in - match t1 with - | IProp _ -> IProp e - | _ -> - let t1 = inj_prop_of_tprop t1 in - TProp (EConstr.mkApp (force mkuprop_op, [|unop; rop; t1|])) - with Not_found -> IProp e - else IProp e + end + | PropUnOp {decl = rop} -> + begin + try + let t1 = trans_prop env evd a.(n-1) in + match t1 with + | IProp _ -> IProp e + | _ -> + let t1 = inj_prop_of_tprop t1 in + TProp (EConstr.mkApp (force mkuprop_op, [|t; rop; t1|])) + with Not_found -> IProp e + end + | _ -> IProp e + with Not_found -> IProp e let unfold n env evd c = let cbv l = CClosure.RedFlags.( Tacred.cbv_norm_flags (mkflags - (fBETA :: fMATCH :: fFIX :: fCOFIX :: fZETA :: List.map fCONST l))) + (fBETA :: fMATCH :: fFIX :: fCOFIX :: fZETA :: List.rev_map fCONST l))) in let unfold_decl = unfold_decl evd in (* Unfold the let binding *) @@ -943,7 +987,7 @@ let unfold n env evd c = Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c in (* Reduce the term *) - let c = cbv (force to_unfold @ unfold_decl) env evd c in + let c = cbv (List.rev_append (force to_unfold) unfold_decl) env evd c in c let trans_check_prop env evd t = @@ -1029,7 +1073,7 @@ let zify_tac = Proofview.Goal.enter (fun gl -> Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"] ; Coqlib.check_required_library ["Coq"; "micromega"; "ZifyInst"] ; - process_all_decl (); + init_cache (); let evd = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in let concl = trans_check_prop env evd (Tacmach.New.pf_concl gl) in @@ -1038,12 +1082,12 @@ let zify_tac = tclTHENOpt concl trans_concl (Tacticals.New.tclTHEN (Tacticals.New.tclTHENLIST - (List.map (fun (h, p, t) -> trans_hyp h p t) hyps)) + (List.rev_map (fun (h, p, t) -> trans_hyp h p t) hyps)) (CstrTable.gen_cstr l)) ) let iter_specs tac = Tacticals.New.tclTHENLIST - (List.fold_right (fun d acc -> tac d :: acc) (Spec.get ()) []) + (List.fold_left (fun acc d -> tac d :: acc) [] (Spec.get ())) let iter_specs (tac: Ltac_plugin.Tacinterp.Value.t) = @@ -1063,11 +1107,11 @@ let sat_constr c d = if Array.length args = 2 then ( let h1 = Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESat.parg1, [|args.(0)|])) + (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) in let h2 = Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESat.parg2, [|args.(1)|])) + (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) in match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with | Some h1, Some h2 -> @@ -1078,7 +1122,7 @@ let sat_constr c d = in let trm = EConstr.mkApp - ( d.ESat.satOK + ( d.ESatT.satOK , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] ) in @@ -1087,20 +1131,28 @@ let sat_constr c d = else Tacticals.New.tclIDTAC | _ -> Tacticals.New.tclIDTAC ) + +let get_all_sat env evd c = + List.fold_left (fun acc e -> + match e with + | (_,Saturate s) -> s::acc + | _ -> acc) [] (HConstr.find_all c !saturate_cache ) + let saturate = Proofview.Goal.enter (fun gl -> + init_cache (); let table = CstrTable.HConstr.create 20 in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in let evd = Tacmach.New.project gl in - process_all_decl (); + let env = Tacmach.New.pf_env gl in let rec sat t = match EConstr.kind evd t with | App (c, args) -> sat c ; Array.iter sat args ; if Array.length args = 2 then - let ds = Saturate.get_all evd c in + let ds = get_all_sat env evd c in if ds = [] then () else ( List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds ) diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index f7844f53bc..54e8f07ddc 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -17,6 +17,7 @@ module BinOp : S module CstOp : S module BinRel : S module PropOp : S +module PropUnOp : S module Spec : S module Saturate : S |