proposition: Lemma eval_Psatz_Sound : forall (l : list NFormula) (env : PolEnv), (forall (f : NFormula), In f l -> eval_nformula env f) -> forall (e : Psatz) (f : NFormula), eval_Psatz l e = Some f -> eval_nformula env f.
proof: Proof. intros l env H e. revert l H. induction e as [e1 IHe1 e2 IHe2 | n|?|? e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2|c|]; simpl ; intros l IN f. - destruct (eval_Psatz l e1) as [f'|] eqn:EP; [|discriminate]. apply IHe2. intros f2 [EQ |IN']. + subst. eapply IHe1; eauto. + eauto. - simpl ; intros H0. destruct (nth_in_or_default n l (Pc cO, Equal)) as [Hin|Heq]. + apply IN. congruence. + inversion H0. rewrite Heq. simpl. now apply (morph0 (SORrm addon)). - intros H0. inversion H0. simpl. unfold eval_pol. rewrite (Psquare_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)); now apply (Rtimes_square_nonneg sor). - case_eq (eval_Psatz l e) ; simpl ; intros ? H0; [intros H1|]. + apply IHe in H0. * apply pexpr_times_nformula_correct with (1:=H0) (2:= H1). * apply IN. + discriminate. - simpl. case_eq (eval_Psatz l e1) ; simpl ; try discriminate. case_eq (eval_Psatz l e2) ; simpl ; try discriminate. intros n H0 n0 H1. apply IHe1 in H1; auto. apply IHe2 in H0; auto. apply (nformula_times_nformula_correct env n0 n); auto. - simpl. case_eq (eval_Psatz l e1) ; simpl ; try discriminate. case_eq (eval_Psatz l e2) ; simpl ; try discriminate. intros n H0 n0 H1. apply IHe1 in H1; auto. apply IHe2 in H0; auto. apply (nformula_plus_nformula_correct env n0 n) ; assumption. - simpl. case_eq (cO [<] c). + intros H0 H1. inversion H1. simpl. rewrite <- (morph0 (SORrm addon)). now apply cltb_sound. + discriminate. - simpl. intros H0. inversion H0. simpl. apply (morph0 (SORrm addon)). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl