examples/disamb.mlw

   1 (** {1 Disambiguation of Plus Expressions }
   2
   3 Author: Quentin Garchery (LRI, Université Paris-Sud)
   4 *)
   5
   6 use int.Int
   7 use list.ListRich
   8
   9 (** Consider the 'concrete' syntax of Plus Expressions containing only :
  10     integers, the symbol PLUS and parentheses. *)
  11
  12 type token = INT | PLUS | LPAREN | RPAREN
  13
  14 (** Plus Expressions are lists of tokens that satisfy the original following
  15     inductive predicate. *)
  16
  17 inductive pe (e : list token) =
  18     | Plus : forall e1 e2. pe e1 -> pe e2 -> pe (e1 ++ Cons PLUS e2)
  19     | Paren : forall e. pe e -> pe (Cons LPAREN (e ++ (Cons RPAREN Nil)))
  20     | Int : pe (Cons INT Nil)
  21
  22 goal pe1 : pe (Cons INT Nil)
  23 goal pe2 : pe (Cons INT (Cons PLUS (Cons INT (Cons PLUS (Cons INT Nil)))))
  24
  25 (** Define another predicate to recognize Plus Expressions but that removes the
  26     ambiguity coming from the associativity of PLUS. *)
  27
  28 inductive pe' (e : list token) =
  29    | Plus' : forall e1 e2. pe' e1 -> pt e2 -> pe' (e1 ++ Cons PLUS e2)
  30    | T' : forall t. pt t -> pe' t
  31 with pt (e : list token) =
  32     | Paren' : forall e. pe' e -> pt (Cons LPAREN (e ++ (Cons RPAREN Nil)))
  33     | Int' : pt (Cons INT Nil)
  34
  35 goal pep1 : pe' (Cons INT Nil)
  36 goal pep2 : pe' (Cons INT (Cons PLUS (Cons INT (Cons PLUS (Cons INT Nil)))))
  37
  38 (** Show that the two predicates recognize the same expressions. *)
  39
  40 (** Strengthen the disambiguation_included formula, making sure the pt predicate
  41     appears. *)
  42
  43 let rec lemma di_str (n : int)
  44     variant { n }
  45     ensures { forall e. (length e <= n /\ pt e) \/ (length e < n /\ pe' e) ->
  46                         pe e }
  47     =
  48     if n <= 0
  49     then ()
  50     else di_str (n-1)
  51
  52 let lemma disambiguation_included (e : list token)
  53     requires { pe' e }
  54     ensures { pe e }
  55     =
  56     di_str (length e + 1)
  57
  58 (** Strengthen the original_included formula and prove it by using mutal
  59     recursion (showing that we can decompose an expression w.r.t its last
  60     toplevel PLUS symbol). *)
  61
  62 let rec lemma oi_str (n : int) (ghost m : int)
  63     variant { n, m }
  64     requires { m > n }
  65     ensures { forall e. length e <= n -> pe e -> pe' e }
  66     = if n > 0 then (decomp_last_plus n (m-1); oi_str (n-1) m)
  67
  68 with ghost decomp_last_plus (n : int) (ghost m : int)
  69      variant { n, m }
  70      requires { m >= n }
  71      ensures { forall e. length e <= n -> pe e -> not pt e ->
  72                exists e1 e2. pe e1 /\ pt e2 /\ e = e1 ++ Cons PLUS e2 }
  73      =
  74      if n > 0 then (decomp_last_plus (n-1) n; oi_str (n-1) n)
  75
  76 lemma original_included :
  77       forall e. pe e -> pe' e
  78
  79 lemma original_equiv_disambiguation :
  80       forall e. pe e <-> pe' e