ImpListImp Extended with Lists

Require Export SfLib.

Imp Programs with Lists

There are only so many numeric functions with interesting properties that have simple proofs. (Of course, there are lots of interesting functions on numbers and they have many interesting properties — this is the whole field of number theory! — but proving these properties often requires developing a lot of supporting lemmas.) In order to able to write a few more programs to reason about, we introduce here an extended version of Imp where variables can range over both numbers and lists of numbers. The basic operations are extended to also include taking the head and tail of lists, and testing lists for nonemptyness.

To do this, we only need to change the definitions of state, aexp, aeval, bexp, and beval. The definitions of com and ceval can be reused verbatim, although we need to copy-and-paste them in the context of the new definitions.

We start by repeating some material from Imp.v.

Repeated Definitions

Inductive id : Type :=
  Id : nat → id.

Definition beq_id id1 id2 :=
  match (id1, id2) with
    (Id n1, Id n2) => beq_nat n1 n2
  end.

Theorem beq_id_refl : ∀ i,
  true = beq_id i i.
Proof.
  intros. destruct i.
  apply beq_nat_refl. Qed.

Theorem beq_id_eq : ∀ i1 i2,
  true = beq_id i1 i2 → i1 = i2.
Proof.
  intros i1 i2 H.
  destruct i1. destruct i2.
  apply beq_nat_eq in H. subst.
  reflexivity. Qed.

Theorem beq_id_false_not_eq : ∀ i1 i2,
  beq_id i1 i2 = false → i1 <> i2.
Proof.
  intros i1 i2 H.
  destruct i1. destruct i2.
  apply beq_nat_false in H.
  intros C. apply H. inversion C. reflexivity. Qed.

Theorem not_eq_beq_id_false : ∀ i1 i2,
  i1 <> i2 → beq_id i1 i2 = false.
Proof.
  intros i1 i2 H.
  destruct i1. destruct i2.
  assert (n <> n0).
    intros C. subst. apply H. reflexivity.
  apply not_eq_beq_false. assumption. Qed.

Definition X : id := Id 0.
Definition Y : id := Id 1.
Definition Z : id := Id 2.

Extensions

Now we come to the key changes.

Rather than evaluating to a nat, an aexp in our new language will evaluate to a value — an element of type val — which can be either a nat or a list of nats.

Similarly, states will now map identifiers to vals rather than nats, so that we can store lists in mutable variables.

Inductive val : Type :=
| VNat : nat → val
| VList : list nat → val.

Definition state := id → val.

Definition empty_state : state := fun _ => VNat 0.
Definition update (st : state) (V:id) (n : val) : state :=
fun V' => if beq_id V V' then n else st V'.

Imp does not have a static type system, so nothing prevents the programmer from e.g. adding two lists or taking the head of a number. We have to decide what to do in such nonsensical situations.

We adopt a simple solution: if an arithmetic function is given a list as an argument we treat the list as if it was the number 0. Similarly, if a list function is given a number as an argument we treat the number as if it was nil. (Cf. Javascript, where adding 3 to the empty list evaluates to 3...)

The two functions asnat and aslist interpret vals in a numeric or a list context; aeval calls these whenever it evaluates an arithmetic or a list operation.

Definition asnat (v : val) : nat :=
  match v with
  | VNat n => n
  | VList _ => 0
  end.

Definition aslist (v : val) : list nat :=
  match v with
  | VNat n => []
  | VList xs => xs
  end.

Now we fill in the definitions of abstract syntax and evaluation functions for arithmetic and boolean expressions.

We extend bexps with an operation to test if a list is nonempty and adapt beval acordingly.

Repeated Definitions

Now we need to repeat a little bit of low-level work from Imp.v, plus the definitions of com and ceval. There are no interesting changes — it's just a matter of repeating the same definitions, lemmas, and proofs in the context of the new definitions of arithmetic and boolean expressions.

(Is all this cutting and pasting really necessary? No: Coq includes a powerful module system that we could use to abstract the repeated definitions with respect to the varying parts. But explaining how it works would distract us from the topic at hand.)

Theorem update_eq : ∀ n V st,
  (update st V n) V = n.
Proof.
  intros n V st.
  unfold update.
  rewrite ← beq_id_refl.
  reflexivity.
Qed.

Theorem update_neq : ∀ V2 V1 n st,
  beq_id V2 V1 = false →
  (update st V2 n) V1 = (st V1).
Proof.
  intros V2 V1 n st Hneq.
  unfold update.
  rewrite → Hneq.
  reflexivity. Qed.

Theorem update_shadow : ∀ x1 x2 k1 k2 (f : state),
   (update (update f k2 x1) k2 x2) k1 = (update f k2 x2) k1.
Proof.
  intros x1 x2 k1 k2 f.
  unfold update.
  destruct (beq_id k2 k1); reflexivity. Qed.

Theorem update_same : ∀ x1 k1 k2 (f : state),
  f k1 = x1 →
  (update f k1 x1) k2 = f k2.
Proof.
  intros x1 k1 k2 f Heq.
  unfold update. subst.
  remember (beq_id k1 k2) as b.
  destruct b.
  Case "true".
    apply beq_id_eq in Heqb. subst. reflexivity.
  Case "false".
    reflexivity. Qed.

Theorem update_permute : ∀ x1 x2 k1 k2 k3 f,
  beq_id k2 k1 = false →
  (update (update f k2 x1) k1 x2) k3 = (update (update f k1 x2) k2 x1) k3.
Proof.
  intros x1 x2 k1 k2 k3 f H.
  unfold update.
  remember (beq_id k1 k3) as b13.
  remember (beq_id k2 k3) as b23.
  apply beq_id_false_not_eq in H.
  destruct b13; try reflexivity.
  Case "true".
    destruct b23; try reflexivity.
    SCase "true".
      apply beq_id_eq in Heqb13.
      apply beq_id_eq in Heqb23.
      subst. apply ex_falso_quodlibet. apply H. reflexivity. Qed.

We can keep exactly the same old definitions of com and ceval.

Inductive com : Type :=
  | CSkip : com
  | CAss : id → aexp → com
  | CSeq : com → com → com
  | CIf : bexp → com → com → com
  | CWhile : bexp → com → com.

Tactic Notation "com_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
  | Case_aux c "IFB" | Case_aux c "WHILE" ].

Notation "'SKIP'" :=
  CSkip.
Notation "l '::=' a" :=
  (CAss l a) (at level 60).
Notation "c1 ; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
  (CIf e1 e2 e3) (at level 80, right associativity).

Reserved Notation "c1 '/' st '⇓' st'" (at level 40, st at level 39).

Inductive ceval : state → com → state → Prop :=
  | E_Skip : ∀ st,
      SKIP / st ⇓ st
  | E_Asgn : ∀ st a1 n l,
      aeval st a1 = n →
      (l ::= a1) / st ⇓ (update st l n)
  | E_Seq : ∀ c1 c2 st st' st'',
      c1 / st ⇓ st' →
      c2 / st' ⇓ st'' →
      (c1 ; c2) / st ⇓ st''
  | E_IfTrue : ∀ st st' b1 c1 c2,
      beval st b1 = true →
      c1 / st ⇓ st' →
      (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
  | E_IfFalse : ∀ st st' b1 c1 c2,
      beval st b1 = false →
      c2 / st ⇓ st' →
      (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
  | E_WhileEnd : ∀ b1 st c1,
      beval st b1 = false →
      (WHILE b1 DO c1 END) / st ⇓ st
  | E_WhileLoop : ∀ st st' st'' b1 c1,
      beval st b1 = true →
      c1 / st ⇓ st' →
      (WHILE b1 DO c1 END) / st' ⇓ st'' →
      (WHILE b1 DO c1 END) / st ⇓ st''

  where "c1 '/' st '⇓' st'" := (ceval st c1 st').

Tactic Notation "ceval_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "E_Skip" | Case_aux c "E_Asgn" | Case_aux c "E_Seq"
  | Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"
  | Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop" ].

Definition loop : com :=
  WHILE BTrue DO
    SKIP
  END.

Theorem loop_never_stops : ∀ st st',
  ~(loop / st ⇓ st').
Proof.
  intros st st' contra. unfold loop in contra.
  remember (WHILE BTrue DO SKIP END) as loopdef.
  ceval_cases (induction contra) Case; try (inversion Heqloopdef).
    Case "E_WhileEnd".
      rewrite → H1 in H. inversion H.
    Case "E_WhileLoop".
      apply IHcontra2. subst. reflexivity. Qed.