proposition: Theorem ExprToPropF : forall e : Expr, exists f : rNat -> bool, f zero = true /\ (forall n : rNat, inExpr n e -> fmap n -> f n = true) /\ (forall n : rNat, inExpr n e -> ~ fmap n -> f n = false).
proof: Proof. intros e; elim e; simpl in |- *; auto with stalmarck. intros r. case (rNatDec r zero); auto with stalmarck. intros H'; exists (fun n : rNat => true). rewrite H'; split; auto with stalmarck; split; auto with stalmarck. intros n H'0; inversion H'0; auto with stalmarck. intros H'1; case H'1; auto with stalmarck. intros H'; case (classic (fmap r)); intros H'1. exists (fun n : rNat => true); simpl in |- *; split; auto with stalmarck; split; auto with stalmarck. intros n H'0; inversion H'0; auto with stalmarck. intros H'2; case H'2; auto with stalmarck. exists (fun n : rNat => match rNatDec r n with | left _ => false | right _ => true end); simpl in |- *. split. case (rNatDec r zero); auto with stalmarck. split; intros n H'0; inversion H'0; case (rNatDec r r); auto with stalmarck. intros H'2 H'3; case H'1; auto with stalmarck. case H'2; auto with stalmarck. intros e0 H'; Elimc H'; intros f E; Elimc E; intros H' H'0; Elimc H'0; intros H'0 H'1. exists f; split; auto with stalmarck. split; intros n H'2; inversion H'2; auto with stalmarck. intros b e0 H' e1 H'0. Elimc H'; intros f E; Elimc E; intros H' H'1; Elimc H'1; intros H'1 H'2. Elimc H'0; intros f0 E; Elimc E; intros H'0 H'3; Elimc H'3; intros H'3 H'4. exists (fun n : rNat => match inExprDec n e0 with | left _ => f n | right _ => f0 n end); simpl in |- *. split. case (inExprDec zero e0); auto with stalmarck. split; intros n H'5 H'6; inversion H'5; case (inExprDec n e0); auto with stalmarck. intros H'7; case H'7; auto with stalmarck. Qed.
imports: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)