summaryrefslogtreecommitdiff
path: root/Test/dafny1/Substitution.dfy
blob: ad39e3f2e87f7803b7f8c647bfcf704d1cc1a3a0 (plain)
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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
datatype List = Nil | Cons(Expr, List);

datatype Expr =
  Const(int) |
  Var(int) |
  Nary(int, List);

static function Subst(e: Expr, v: int, val: int): Expr
{
  match e
  case Const(c) => e
  case Var(x) => if x == v then Expr.Const(val) else e
  case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
}

static function SubstList(l: List, v: int, val: int): List
{
  match l
  case Nil => l
  case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
}

static ghost method Theorem(e: Expr, v: int, val: int)
  ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);
{
  match e {
    case Const(c) =>
    case Var(x) =>
    case Nary(op, args) =>
      Lemma(args, v, val);
  }
}

static ghost method Lemma(l: List, v: int, val: int)
  ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);
{
  match l {
    case Nil =>
    case Cons(e, tail) =>
      Theorem(e, v, val);
      Lemma(tail, v, val);
  }
}

// -------------------------------

datatype Expression =
  Const(int) |
  Var(int) |
  Nary(int, seq<Expression>);

static function Substitute(e: Expression, v: int, val: int): Expression
  decreases e;
{
  match e
  case Const(c) => e
  case Var(x) => if x == v then Expression.Const(val) else e
  case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
}

static function SubstSeq(/*ghost*/ parent: Expression,
                         q: seq<Expression>, v: int, val: int): seq<Expression>
  requires (forall a :: a in q ==> a < parent);
  decreases parent, q;
{
  if q == [] then [] else
  SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]
}

static ghost method TheoremSeq(e: Expression, v: int, val: int)
  ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);
{
  match e {
    case Const(c) =>
    case Var(x) =>
    case Nary(op, args) =>
      ghost var seArgs := SubstSeq(e, args, v, val);
      LemmaSeq(e, args, v, val);

      ghost var se := Substitute(e, v, val);
      ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
      LemmaSeq(se, seArgs, v, val);

      var N := |args|;
      var j := 0;
      while (j < N)
        invariant j <= N;
        invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
      {
        TheoremSeq(args[j], v, val);
        j := j + 1;
      }
      assert seArgs == seArgs2;
  }
}

static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
  requires (forall a :: a in q ==> a < parent);
  ensures |SubstSeq(parent, q, v, val)| == |q|;
  ensures (forall k :: 0 <= k && k < |q| ==>
            SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));
{
  if (q == []) {
  } else {
    LemmaSeq(parent, q[..|q|-1], v, val);
  }
}