diff options
Diffstat (limited to 'plugins/micromega/RingMicromega.v')
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 195 |
1 files changed, 174 insertions, 21 deletions
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index b10cf784..4af65086 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.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 *) @@ -308,7 +308,7 @@ Definition map_option (A B:Type) (f : A -> option B) (o : option A) : option B : | Some x => f x end. -Implicit Arguments map_option [A B]. +Arguments map_option [A B] f o. Definition map_option2 (A B C : Type) (f : A -> B -> option C) (o: option A) (o': option B) : option C := @@ -318,7 +318,7 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C) | Some x , Some x' => f x x' end. -Implicit Arguments map_option2 [A B C]. +Arguments map_option2 [A B C] f o o'. Definition Rops_wd := mk_reqe rplus rtimes ropp req sor.(SORplus_wd) @@ -355,6 +355,7 @@ Fixpoint eval_Psatz (l : list NFormula) (e : Psatz) {struct e} : option NFormula | PsatzZ => Some (Pc cO, Equal) (* Just to make life easier *) end. + Lemma pexpr_times_nformula_correct : forall (env: PolEnv) (e: PolC) (f f' : NFormula), eval_nformula env f -> pexpr_times_nformula e f = Some f' -> eval_nformula env f'. @@ -490,6 +491,99 @@ Fixpoint xhyps_of_psatz (base:nat) (acc : list nat) (prf : Psatz) : list nat := | PsatzIn n => if ge_bool n base then (n::acc) else acc end. +Fixpoint nhyps_of_psatz (prf : Psatz) : list nat := + match prf with + | PsatzC _ | PsatzZ | PsatzSquare _ => nil + | PsatzMulC _ prf => nhyps_of_psatz prf + | PsatzAdd e1 e2 | PsatzMulE e1 e2 => nhyps_of_psatz e1 ++ nhyps_of_psatz e2 + | PsatzIn n => n :: nil + end. + + +Fixpoint extract_hyps (l: list NFormula) (ln : list nat) : list NFormula := + match ln with + | nil => nil + | n::ln => nth n l (Pc cO, Equal) :: extract_hyps l ln + end. + +Lemma extract_hyps_app : forall l ln1 ln2, + extract_hyps l (ln1 ++ ln2) = (extract_hyps l ln1) ++ (extract_hyps l ln2). +Proof. + induction ln1. + reflexivity. + simpl. + intros. + rewrite IHln1. reflexivity. +Qed. + +Ltac inv H := inversion H ; try subst ; clear H. + +Lemma nhyps_of_psatz_correct : forall (env : PolEnv) (e:Psatz) (l : list NFormula) (f: NFormula), + eval_Psatz l e = Some f -> + ((forall f', In f' (extract_hyps l (nhyps_of_psatz e)) -> eval_nformula env f') -> eval_nformula env f). +Proof. + induction e ; intros. + (*PsatzIn*) + simpl in *. + apply H0. intuition congruence. + (* PsatzSquare *) + simpl in *. + inv H. + simpl. + unfold eval_pol. + rewrite (Psquare_ok sor.(SORsetoid) Rops_wd + (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)); + now apply (Rtimes_square_nonneg sor). + (* PsatzMulC *) + simpl in *. + case_eq (eval_Psatz l e). + intros. rewrite H1 in H. simpl in H. + apply pexpr_times_nformula_correct with (2:= H). + apply IHe with (1:= H1); auto. + intros. rewrite H1 in H. simpl in H ; discriminate. + (* PsatzMulE *) + simpl in *. + revert H. + case_eq (eval_Psatz l e1). + case_eq (eval_Psatz l e2) ; simpl ; intros. + apply nformula_times_nformula_correct with (3:= H2). + apply IHe1 with (1:= H1) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + apply IHe2 with (1:= H) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + discriminate. simpl. discriminate. + (* PsatzAdd *) + simpl in *. + revert H. + case_eq (eval_Psatz l e1). + case_eq (eval_Psatz l e2) ; simpl ; intros. + apply nformula_plus_nformula_correct with (3:= H2). + apply IHe1 with (1:= H1) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + apply IHe2 with (1:= H) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + discriminate. simpl. discriminate. + (* PsatzC *) + simpl in H. + case_eq (cO [<] c). + intros. rewrite H1 in H. inv H. + unfold eval_nformula. simpl. + rewrite <- addon.(SORrm).(morph0). now apply cltb_sound. + intros. rewrite H1 in H. discriminate. + (* PsatzZ *) + simpl in *. inv H. + unfold eval_nformula. simpl. + apply addon.(SORrm).(morph0). +Qed. + + + + + (* roughly speaking, normalise_pexpr_correct is a proof of forall env p, eval_pexpr env p == eval_pol env (normalise_pexpr p) *) @@ -546,6 +640,7 @@ apply cleb_sound in H1. now apply -> (Rle_ngt sor). apply cltb_sound in H1. now apply -> (Rlt_nge sor). Qed. + Definition check_normalised_formulas : list NFormula -> Psatz -> bool := fun l cm => match eval_Psatz l cm with @@ -592,16 +687,17 @@ end. Definition eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe. -Record Formula : Type := { - Flhs : PExpr C; +Record Formula (T:Type) : Type := { + Flhs : PExpr T; Fop : Op2; - Frhs : PExpr C + Frhs : PExpr T }. -Definition eval_formula (env : PolEnv) (f : Formula) : Prop := +Definition eval_formula (env : PolEnv) (f : Formula C) : Prop := let (lhs, op, rhs) := f in (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs). + (* We normalize Formulas by moving terms to one side *) Definition norm := norm_aux cO cI cplus ctimes cminus copp ceqb. @@ -610,7 +706,7 @@ Definition psub := Psub cO cplus cminus copp ceqb. Definition padd := Padd cO cplus ceqb. -Definition normalise (f : Formula) : NFormula := +Definition normalise (f : Formula C) : NFormula := let (lhs, op, rhs) := f in let lhs := norm lhs in let rhs := norm rhs in @@ -623,7 +719,7 @@ let (lhs, op, rhs) := f in | OpLt => (psub rhs lhs, Strict) end. -Definition negate (f : Formula) : NFormula := +Definition negate (f : Formula C) : NFormula := let (lhs, op, rhs) := f in let lhs := norm lhs in let rhs := norm rhs in @@ -659,7 +755,7 @@ Qed. Theorem normalise_sound : - forall (env : PolEnv) (f : Formula), + forall (env : PolEnv) (f : Formula C), eval_formula env f -> eval_nformula env (normalise f). Proof. intros env f H; destruct f as [lhs op rhs]; simpl in *. @@ -673,7 +769,7 @@ now apply -> (Rlt_lt_minus sor). Qed. Theorem negate_correct : - forall (env : PolEnv) (f : Formula), + forall (env : PolEnv) (f : Formula C), eval_formula env f <-> ~ (eval_nformula env (negate f)). Proof. intros env f; destruct f as [lhs op rhs]; simpl. @@ -687,9 +783,9 @@ rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). Qed. -(** Another normalistion - this is used for cnf conversion **) +(** Another normalisation - this is used for cnf conversion **) -Definition xnormalise (t:Formula) : list (NFormula) := +Definition xnormalise (t:Formula C) : list (NFormula) := let (lhs,o,rhs) := t in let lhs := norm lhs in let rhs := norm rhs in @@ -705,16 +801,16 @@ Definition xnormalise (t:Formula) : list (NFormula) := Require Import Tauto. -Definition cnf_normalise (t:Formula) : cnf (NFormula) := +Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). Add Ring SORRing : sor.(SORrt). -Lemma cnf_normalise_correct : forall env t, eval_cnf (eval_nformula env) (cnf_normalise t) -> eval_formula env t. +Lemma cnf_normalise_correct : forall env t, eval_cnf eval_nformula env (cnf_normalise t) -> eval_formula env t. Proof. unfold cnf_normalise, xnormalise ; simpl ; intros env t. - unfold eval_cnf. + unfold eval_cnf, eval_clause. destruct t as [lhs o rhs]; case_eq o ; simpl; repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; generalize (eval_pexpr env lhs); @@ -730,7 +826,7 @@ Proof. rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). auto. Qed. -Definition xnegate (t:Formula) : list (NFormula) := +Definition xnegate (t:Formula C) : list (NFormula) := let (lhs,o,rhs) := t in let lhs := norm lhs in let rhs := norm rhs in @@ -743,13 +839,13 @@ Definition xnegate (t:Formula) : list (NFormula) := | OpLe => (psub rhs lhs,NonStrict) :: nil end. -Definition cnf_negate (t:Formula) : cnf (NFormula) := +Definition cnf_negate (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnegate t). -Lemma cnf_negate_correct : forall env t, eval_cnf (eval_nformula env) (cnf_negate t) -> ~ eval_formula env t. +Lemma cnf_negate_correct : forall env t, eval_cnf eval_nformula env (cnf_negate t) -> ~ eval_formula env t. Proof. unfold cnf_negate, xnegate ; simpl ; intros env t. - unfold eval_cnf. + unfold eval_cnf, eval_clause. destruct t as [lhs o rhs]; case_eq o ; simpl; repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; generalize (eval_pexpr env lhs); @@ -841,6 +937,63 @@ Proof. Qed. +(** Sometimes it is convenient to make a distinction between "syntactic" coefficients and "real" +coefficients that are used to actually compute *) + + + +Variable S : Type. + +Variable C_of_S : S -> C. + +Variable phiS : S -> R. + +Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). + +Fixpoint map_PExpr (e : PExpr S) : PExpr C := + match e with + | PEc c => PEc (C_of_S c) + | PEX p => PEX _ p + | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) + | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) + | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) + | PEopp e => PEopp (map_PExpr e) + | PEpow e n => PEpow (map_PExpr e) n + end. + +Definition map_Formula (f : Formula S) : Formula C := + let (l,o,r) := f in + Build_Formula (map_PExpr l) o (map_PExpr r). + + +Definition eval_sexpr (env : PolEnv) (e : PExpr S) : R := + PEeval rplus rtimes rminus ropp phiS pow_phi rpow env e. + +Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop := + let (lhs, op, rhs) := f in + (eval_op2 op) (eval_sexpr env lhs) (eval_sexpr env rhs). + +Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (map_PExpr s). +Proof. + unfold eval_pexpr, eval_sexpr. + induction s ; simpl ; try (rewrite IHs1 ; rewrite IHs2) ; try reflexivity. + apply phi_C_of_S. + rewrite IHs. reflexivity. + rewrite IHs. reflexivity. +Qed. + +(** equality migth be (too) strong *) +Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). +Proof. + destruct f. + simpl. + repeat rewrite eval_pexprSC. + reflexivity. +Qed. + + + + (** Some syntactic simplifications of expressions *) @@ -881,4 +1034,4 @@ End Micromega. (* Local Variables: *) (* coding: utf-8 *) -(* End: *)
\ No newline at end of file +(* End: *) |