proposition: Theorem ExprToPropF2 : forall (e : Expr) (f : rNat -> bool), (forall n : rNat, inExpr n e -> fmap n -> f n = true) -> (forall n : rNat, inExpr n e -> ~ fmap n -> f n = false) -> (Eval f e = true -> ExprToProp e) /\ (Eval f e = false -> ~ ExprToProp e).
proof: Proof. intros e; Elimc e; simpl in |- *; auto with stalmarck. intros r f H' H'0; split; case (classic (fmap r)); auto with stalmarck. intros H'1 H'2; absurd (f r = false); auto with stalmarck. rewrite H'2; red in |- *; intros H'3; discriminate. intros H'1 H'2; absurd (f r = true); auto with stalmarck. rewrite H'2; red in |- *; intros H'3; discriminate. intros e H' f H'0 H'1; split; intros H'2; auto with stalmarck. elim (H' f); [ intros H'6 H'7; apply H'7 | idtac | idtac ]; auto with stalmarck. generalize H'2; case (Eval f e); auto with stalmarck. red in |- *; intros H'3; Contradict H'3. elim (H' f); [ intros H'4 H'5; apply H'4 | idtac | idtac ]; auto with stalmarck. generalize H'2; case (Eval f e); auto with stalmarck. intros b e H' e0 H'0 f H'1 H'2. generalize (H' f) (H'0 f); clear H' H'0; case b; simpl in |- *. case (Eval f e); simpl in |- *; auto with stalmarck. case (Eval f e0); simpl in |- *; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. split. elim H'; auto with stalmarck. elim H'0; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; intros H'4; Elimc H'4; intros H'4 H'5. absurd (ExprToProp e0); auto with stalmarck. elim H'0; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; intros H'4; Elimc H'4; intros H'4 H'5. absurd (ExprToProp e); auto with stalmarck. elim H'; auto with stalmarck. case (Eval f e); simpl in |- *; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. elim H'; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. elim H'0; auto with stalmarck. red in |- *; intros H'4; Elimc H'4; intros H'4. absurd (ExprToProp e); auto with stalmarck. elim H'; auto with stalmarck. absurd (ExprToProp e0); auto with stalmarck. elim H'0; auto with stalmarck. case (Eval f e); case (Eval f e0); simpl in |- *; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. elim H'0; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; intros H'4. absurd (ExprToProp e0); auto with stalmarck. elim H'0; auto with stalmarck. elim H'; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. elim H'0; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. intros H'4; absurd (ExprToProp e); auto with stalmarck. elim H'; auto with stalmarck. case (Eval f e); case (Eval f e0); simpl in |- *; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; split; elim H'0; elim H'; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; intros H'4; absurd (ExprToProp e); auto with stalmarck. red in |- *; intros H'5; absurd (ExprToProp e0); auto with stalmarck. elim H'0; auto with stalmarck. elim H'4; auto with stalmarck. elim H'; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; intros H'4; absurd (ExprToProp e); auto with stalmarck. elim H'; auto with stalmarck. cut (ExprToProp e0); auto with stalmarck. elim H'4; auto with stalmarck. elim H'0; auto with stalmarck. intros H' H'0; split; intros H'3; try discriminate. red in |- *; split; intros H'4. absurd (ExprToProp e); auto with stalmarck; elim H'; auto with stalmarck. absurd (ExprToProp e0); auto with stalmarck; elim H'0; auto with stalmarck. Qed.
imports: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)