proposition: Theorem checkTrace : forall (e : Expr) (T : Trace), match makeTriplets (norm e) with | tRC L r n => match fInT (getT (buildL L)) T with | true => match addEqMem (rArrayInit _ (fun r => class nil)) r rZFalse with | triple Ar1 true L1 => Tautology e | triple Ar1 false L1 => match evalTraceF T Ar1 with | triple Ar' false L => True | triple Ar' true L => Tautology e end end | false => True end end.
proof: Proof. intros e T; CaseEq (makeTriplets (norm e)). intros l r r0. CaseEq (fInT (getT (buildL l)) T); auto with stalmarck. CaseEq (addEqMem (rArrayInit vM (fun _ : rNat => class nil)) r rZFalse). intros r1 b; case b; auto with stalmarck. intros l0 H' H'0 H'1. case (TautoRTauto e). intros H'3 H'4; apply H'4; auto with stalmarck. case (rTautotTauto (norm e)). intros H'5 H'6; apply H'6; auto with stalmarck. red in |- *; rewrite H'1. apply stalmarckGivesValidEquation with (S := addEq (r, rZFalse) nil); auto with stalmarck. generalize (addEqMemCorrect (rArrayInit vM (fun _ : rNat => class nil)) r rZFalse nil). rewrite H'; auto with stalmarck. intros H'2; apply H'2; auto with stalmarck. apply rIwF; auto with stalmarck. exact initCorrect; auto with stalmarck. CaseEq (evalTraceF T r1). intros r2 b0; case b0; auto with stalmarck. intros l0 H' l1 H'0 H'1 H'2. case (TautoRTauto e). intros H'3 H'4; apply H'4; auto with stalmarck. case (rTautotTauto (norm e)). intros H'5 H'6; apply H'6; auto with stalmarck. red in |- *; rewrite H'2. generalize (TraceCorrect r1 T l). rewrite H'; auto with stalmarck. generalize (addEqMemCorrect (rArrayInit vM (fun _ : rNat => class nil)) r rZFalse nil). rewrite H'0; auto with stalmarck. intros H'7; Elimc H'7; [ intros H'7 H'8; Elimc H'8; intros H'8 H'9; Elimc H'9; intros H'9 H'10 | idtac | idtac ]; auto with stalmarck. intros H'11; lapply H'11; [ intros H'12; elim (H'12 (addEq (r, rZFalse) nil)); [ intros S' E; Elimc E; intros H'13 H'14; clear H'11 | clear H'11 | clear H'11 ] | clear H'11 ]; auto with stalmarck. apply stalmarckGivesValidEquation with (S := S'); auto with stalmarck. apply fInTCorrect with (f := getT (buildL l)); auto with stalmarck. intros n; apply getTCorrect; auto with stalmarck. apply rIwF; auto with stalmarck. exact initCorrect; auto with stalmarck. Qed.
imports: Stalmarck(makeTriplet)