McCarthy-Painter/LinearMemory.v at master · pa-ba/McCarthy-Painter · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
Require Import Memory.
Require Import ZArith.
Require Import FunctionalExtensionality.
Module LinearMemory <: Memory.
Definition adr := nat.
Definition first := 0.
Definition next := S.


Definition Mem := adr -> nat.

Definition get r (m : Mem) := m r.
Definition set r v (m : Mem) r' :=
  if beq_nat r' r then v else m r'.


Definition empty : Mem := fun _ => 0.

Definition free : adr -> Mem -> Mem :=
  fun r m => set r 0 m.

Definition isFreeFrom : adr -> Mem -> Prop :=
  fun r m => forall r', r <= r' -> m r' = 0.

Lemma isFreeFrom_free : forall (r : adr) (m : Mem) (n : nat), isFreeFrom r m -> free r (set r n m) = m.
Proof.
  intros. unfold free, isFreeFrom, set in *. apply functional_extensionality. intros.
  remember (beq_nat x r) as b. destruct b.
  - symmetry in Heqb. apply beq_nat_true in Heqb. subst. erewrite H;auto.
  - reflexivity.
Qed.

Lemma isFreeFrom_set : forall (r : adr) (m : Mem) (n : nat), isFreeFrom r m  ->  isFreeFrom (next r) (set r n m).
Proof.
  unfold isFreeFrom, set, next. intros.  remember (beq_nat r' r) as b. destruct b;symmetry in Heqb.
  - apply beq_nat_true in Heqb. omega.
  - apply beq_nat_false in Heqb. apply H. omega.
Qed.

Lemma get_set : forall (r : adr) (m : Mem) (n : nat), get r (set r n m) = n.
Proof.
  intros. unfold get, set. rewrite <- beq_nat_refl. reflexivity.
Qed.

Lemma isFreeFrom_first : isFreeFrom first empty.
Proof.
  unfold isFreeFrom, first, empty. auto.
Qed.
End LinearMemory.

Module LinearMemoryExt <: MemoryExt.
Include LinearMemory.

Lemma get_set' : forall (r : adr) (r' : adr) (m : Mem) (n : nat),
    r <> r' -> get r (set r' n m) = get r m.
Proof.
  intros.
  unfold get, set. remember (r =? r') as b. destruct b.
  - symmetry in Heqb. apply beq_nat_true in Heqb. contradiction.
  - reflexivity.
Qed.


Lemma next_fresh : forall (r r' : adr), lta adr next r r' -> r <> r'.
Proof.
  intros. apply Nat.lt_neq.
  intros. induction H; auto.
Qed.

End LinearMemoryExt.