proposition: Lemma cexec_infinite_loop: forall s, ~ exists s', cexec s (WHILE TRUE SKIP) s'.
proof: Proof. assert (A: forall s c s', cexec s c s' -> c = WHILE TRUE SKIP -> False). { induction 1; intros EQ; inversion EQ. - subst b c. cbn in H. discriminate. - subst b c. apply IHcexec2. auto. } intros s (s' & EXEC). apply A with (s := s) (c := WHILE TRUE SKIP) (s' := s'); auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)