Software Foundations: More Automation

Auto.v

(* https://gist.github.com/pedrominicz/f7bb82bcf9ba2bcefbca665219346e7a *)
Require Import Maps.
Import Total.
(* https://gist.github.com/pedrominicz/ffc64ced0d034b8edd33332eb90ccc65 *)
Require Import Imp.

Theorem eval_deterministic : forall s s1 s2 c,
  s =[ c ]=> s1 -> s =[ c ]=> s2 -> s1 = s2.
Proof with subst; try discriminate; try congruence; auto.
  intros s s1 s2 c H1 H2.
  generalize dependent s2.
  induction H1; intros; inversion H2...
  - assert (s2 = s5) as H...
  - assert (s2 = s5) as H...
Qed.

Ltac eq :=
match goal with
H1 : forall x, ?P x -> ?L = ?R,
H2 : ?P ?X
|- _ => rewrite (H1 X H2) in *
end.

Theorem eval_deterministic' : forall s s1 s2 c,
  s =[ c ]=> s1 -> s =[ c ]=> s2 -> s1 = s2.
Proof with subst; auto; try congruence.
  intros s s1 s2 c H1 H2.
  generalize dependent s2.
  induction H1; intros; inversion H2; repeat eq; congruence.
Qed.

Example example_1 :
  empty =[
    x ::= 2;;
    test x <= 1
      then y ::= 3
      else z ::= 4
    end
  ]=> (z !-> 4; x !-> 2).
Proof.
  eapply seq.
  - apply assign. reflexivity.
  - apply test_false.
    + reflexivity.
    + apply assign. reflexivity.
Qed.

Example example_2 :
  empty =[
    x ::= 2;;
    while ~(x = 0) do
      y ::= x + y;;
      x ::= x - 1
    end
  ]=> (x !-> 0; y !-> 3; x !-> 1; y !-> 2; x !-> 2).
Proof.
  eapply seq.
  - apply assign. reflexivity.
  - eapply while_true.
    + reflexivity.
    + eapply seq; apply assign; reflexivity.
    + eapply while_true.
      * reflexivity.
      * eapply seq; apply assign; reflexivity.
      * apply while_false. reflexivity.
Qed.

Hint Constructors eval : core.
Hint Transparent map : core.
Hint Transparent state : core.

Example example_3 : exists s,
  (y !-> 2; x !-> 1) =[
    test x <= y
      then z ::= y - x
      else y ::= x + z
    end
  ]=> s.
Proof. eauto. Qed.