proposition: Lemma beval_OR: forall s b1 b2, beval (OR b1 b2) s = beval b1 s || beval b2 s.
proof: Proof. intros; cbn. Abort. Inductive com: Type := | SKIP | ASSIGN (x: ident) (a: aexp) | SEQ (c1: com) (c2: com) | IFTHENELSE (b: bexp) (c1: com) (c2: com) | WHILE (b: bexp) (c1: com). Infix ";;" := SEQ (at level 80, right associativity). Definition Euclidean_division := ASSIGN "r" (VAR "a") ;; ASSIGN "q" (CONST 0) ;; WHILE (LESSEQUAL (VAR "b") (VAR "r")) (ASSIGN "r" (MINUS (VAR "r") (VAR "b")) ;; ASSIGN "q" (PLUS (VAR "q") (CONST 1))). Definition update (x: ident) (v: Z) (s: store) : store := fun y => if string_dec x y then v else s y. Lemma update_same: forall x v s, (update x v s) x = v. Proof. unfold update; intros. destruct (string_dec x x); congruence. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)