Reduce the size of proof

2019-02-04 02:30:43 +09:00 · 2019-02-04 02:30:43 +09:00 · d3adae072c
--- a/src/bitvector.lean
+++ b/src/bitvector.lean
@ -43,10 +43,13 @@ def of_int (sz:size) : ℤ → bitvector sz
 | x@(int.neg_succ_of_nat p) :=
  ⟨(((2 ^ sz.val) - p - 1) % (2^sz.val)), ♯⟩

+@[simp]
 def all_one (sz:size) : bitvector sz := of_int sz (all_one_nat sz)

+@[simp]
 def int_min (sz:size) : bitvector sz := of_int sz (int_min_nat sz)

+@[simp]
 def zero (sz:size) : bitvector sz := of_int sz 0

 def of_bool (b:bool) : bitvector (size.one) := of_int size.one (cond b 1 0)
--- a/src/freevar.lean
+++ b/src/freevar.lean
@ -108,6 +108,7 @@ namespace env
  def add_b (e:env) (name:string) (b:bool):env :=
    {bv := e.bv, b := (λ n, if n = name then some b else e.b n)}

+  @[simp]
  mutual def replace_sbv, replace_sb
  with replace_sbv: Π (η:env) {sz:size}, sbitvec sz → sbitvec sz
  | η sz x@(sbitvec.var _ name) :=
@ -201,8 +202,8 @@ namespace env
    have 0 < sbitvec.sizeof sz x, by apply sbitvec.decr_sbitvec,
    sbool.ult (replace_sbv η x) (replace_sbv η y)
  | η x := x
-  

+  @[simp, reducible]
  def replace_valty (η:env) (v:irsem.valty irsem_smt) :=
    match v with
    | irsem.valty.ival sz i p :=
--- a/src/smtexpr.lean
+++ b/src/smtexpr.lean
@ -90,14 +90,19 @@ def of_int (sz:size) : ℤ → sbitvec sz
 | x@(int.neg_succ_of_nat p) :=
  sbitvec.const sz (((2 ^ sz.val) - p - 1) % (2^sz.val))

+@[simp]
 def one (sz:size) : sbitvec sz := of_int sz 1

+@[simp]
 def zero (sz:size) : sbitvec sz := of_int sz 0

+@[simp]
 def intmin (sz:size) : sbitvec sz := of_int sz (int_min_nat sz)

+@[simp]
 def intmax (sz:size) : sbitvec sz := of_int sz (int.of_nat ((2^(sz.val-1))-1))

+@[simp]
 def uintmax (sz:size) : sbitvec sz := of_int sz (all_one_nat sz)

 def of_bool (b:sbool) : sbitvec (size.one) :=
@ -127,9 +132,11 @@ end

 variable {sz:size}

+@[simp]
 def mk_zext (m:size) (a:sbitvec sz): sbitvec (sz.add m) :=
  sbitvec.zext (sz.add m) a

+@[simp]
 def mk_sext (m:size) (a:sbitvec sz): sbitvec (sz.add m) :=
  sbitvec.sext (sz.add m) a

--- a/src/spec/closed.lean
+++ b/src/spec/closed.lean
@ -63,7 +63,6 @@ lemma closed_b_never_var: ∀ s, ¬ closed_b (sbool.var s)
  unfold env.add_b at H',
  unfold freevar.env.replace_sb at H',
  simp at H',
-  unfold env.replace_sb._match_1 at H',
  cases H'
 end

@ -76,7 +75,6 @@ lemma closed_bv_never_var: ∀ sz s, ¬ closed_bv (sbitvec.var sz s)
  unfold env.add_bv at H',
  unfold freevar.env.replace_sbv at H',
  simp at H',
-  unfold env.replace_sbv._match_1 at H',
  cases H'
 end

@ -169,7 +167,6 @@ lemma closed_b_var_add2: ∀ (η:freevar.env) (v:bool) (s:string),
  simp,
  intros,
  generalize Hb': (η.b s) = b',
-  unfold env.replace_sb._match_1 at *,
  unfold closed_b,
  intros, cases v, refl, refl
 end
@ -204,14 +201,13 @@ lemma closed_bv_var_add2: ∀ (η:freevar.env) sz v (s:string),
  closed_bv ((η.add_bv s v)⟦sbitvec.var sz s⟧)
 := begin
  unfold env.add_bv,
-  unfold freevar.env.replace_sbv,
-  simp,
  intros,
  generalize Hb': (η.b s) = b',
-  unfold env.replace_sbv._match_1 at *,
  unfold closed_bv,
-  intros, cases v; unfold sbitvec.of_int;
-  unfold freevar.env.replace_sbv
+  intros, cases v;
+  unfold freevar.env.replace_sbv; simp,
+  { unfold sbitvec.of_int, unfold env.replace_sbv },
+  { unfold sbitvec.of_int, unfold env.replace_sbv },
 end

 lemma ival_closed: ∀ sz vn pn (η:freevar.env) z b,
@ -224,18 +220,12 @@ lemma ival_closed: ∀ sz vn pn (η:freevar.env) z b,
  unfold env.add_b,
  unfold env.add_bv,
  simp,
-  unfold freevar.env.replace_valty,
-  unfold freevar.env.replace_sb,
-  unfold freevar.env.replace_sbv,
-  simp,
  split,
  {
-    unfold env.replace_sbv._match_1,
    cases z; unfold sbitvec.of_int;
    unfold freevar.env.replace_sbv
  },
  {
-    unfold env.replace_sb._match_1,
    rw env.replace_sb_of_bool
  }
 end
@ -289,17 +279,8 @@ lemma closed_regfile_update_split: ∀ {rf:regfile irsem_smt} {n} {v},
    unfold regfile.apply_to_values at *,
    simp at HC,
    split,
-    {
-      intros,
-      have HC := HC η,
-      injection HC
-    },
-    {
-      intros,
-      have HC := HC η,
-      injection HC,
-      injection h_1
-    }
+    { intros, have HC := HC η, injection HC },
+    { intros, have HC := HC η, injection HC, injection h_1 }
  },
  {
    intros HC η,
@ -307,11 +288,13 @@ lemma closed_regfile_update_split: ∀ {rf:regfile irsem_smt} {n} {v},
    have HC1 := HC1 η,
    have HC2 := HC2 η,
    unfold regfile.apply_to_values at *,
-    simp,
+    simp at *,
    rw HC1, rw HC2
  }
 end

+
+
 -- TODO 1: Merge closed_b_add_b and closed_bv_add_b into a single
 -- theorem (I tried merging them
 -- but it raised excessive memory consumption error.)
--- a/src/spec/customlemmas.lean
+++ b/src/spec/customlemmas.lean
@ -34,6 +34,9 @@ def is_poison: irsem.valty irsem_exec → Prop
 set_option eqn_compiler.zeta true
 set_option pp.proofs true

+local attribute [simp] option.bind irsem.step irsem.step_bop
+  irsem.bop irsem.bop_ub irsem.irstate.updateub irsem.irstate.updatereg
+
 lemma never_poison:
  ∀ isz name op1 op2 st st' val
    (HSTEP:step st (udiv isz name op1 op2) = some st')
@ -47,53 +50,31 @@ lemma never_poison:
    injection HNOUB, clear HNOUB,
  cases op2, simp at *,
  {
-    unfold irsem.step at HSTEP,
    cases (irsem.get_value irsem_exec (ub, regs) op1 (ty.int isz)) with val1;
      unfold has_bind.bind at *; unfold option.bind at *,
    injection HSTEP,
-    rw ← HVAL at HSTEP, unfold option.bind at HSTEP,
-    unfold irsem.step_bop at HSTEP,
+    rw ← HVAL at HSTEP, simp at HSTEP,
    cases val1 with isz1 ii1 ip1,
    cases val with isz2 ii2 ip2,
+    simp at HSTEP,
    have HISZDEC:decidable (isz1 = isz2), apply_instance,
-    cases HISZDEC;
-      unfold irsem.step_bop._match_1 at HSTEP;
-      unfold irsem.bop at HSTEP;
-      unfold irsem.step_bop._match_2 at HSTEP;
-      unfold irsem.bop_val at HSTEP,
-    { rw dif_neg at HSTEP, injection HSTEP
-    },
-    {
-      rw (dif_pos HISZDEC) at HSTEP,
+    cases HISZDEC; unfold irsem.bop_val at HSTEP,
+    { rw dif_neg at HSTEP, injection HSTEP },
+    { rw (dif_pos HISZDEC) at HSTEP,
      injection HSTEP with HSTEP', clear HSTEP,
-      generalize HH:
-  (irsem.bop_ub irsem_exec isz1 bopcode.udiv ii1 ip1 (cast (by rw HISZDEC) ii2) ip2)
-    = eub,
-      rw HH at HSTEP',
-      unfold irsem.irstate.updateub at HSTEP',
-      unfold irsem.irstate.updatereg at HSTEP',
-      simp at HSTEP', injection HSTEP' with HUB HREG,
-      cases eub, cases ub; injection HUB,
-      -- now let's unfold irsem.bop_ub.
-      unfold irsem.bop_ub at HH,
-      have HDIV: bop_isdiv bopcode.udiv = tt, by simp,
-      rw (if_pos HDIV) at HH,
-      simp at *,
-      cases ip2,
-      { -- if dividend was poison..
-        unfold_coes at HH, unfold has_and.and at HH,
-        unfold bool_like.and at HH, simp at HH, exfalso, exact HH
-      },
-      {
-        simp
-      }
+      cases ub; cases ip2,
+      any_goals {
+        -- if dividend was poison or previous state was ub..
+        unfold_coes at HSTEP', unfold has_and.and at HSTEP',
+        unfold bool_like.and at HSTEP', simp at HSTEP', injection HSTEP' with HH _,
+        injection HH },
+      { simp }
    }
  },
  {
-    simp at HVAL, unfold irsem.get_value at HVAL,
+    simp at HVAL,
    cases op2,
-    dunfold irsem.get_value._match_1 at HVAL,
-    dunfold irsem.get_value._match_2 at HVAL,
+    unfold irsem.get_value at HVAL,
    have HSZDEC1: decidable (0 < isz), apply_instance,
    cases HSZDEC1,
    { rw (dif_neg HSZDEC1) at HVAL, injection HVAL },
--- a/src/spec/freevar.lean
+++ b/src/spec/freevar.lean
@ -460,11 +460,10 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧
    intros,
    unfold freevar.env.replace_sb,
    unfold freevar.env.empty,
-    simp,
-    unfold freevar.env.replace_sb._match_1
+    simp, done
  },
  any_goals {
-    intros b H, unfold freevar.env.replace_sb, rw H, done
+    intros b H, unfold freevar.env.replace_sb, rw H
  },
  any_goals {
    intros b1 b2 H1 H2, unfold freevar.env.replace_sb, rw [H1, H2], done
@ -486,8 +485,7 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧
    intros,
    unfold freevar.env.replace_sbv,
    unfold freevar.env.empty,
-    simp,
-    unfold freevar.env.replace_sbv._match_1
+    simp, done
  },
  any_goals {
    intros sz v' sz' H,
@ -505,6 +503,7 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧
  }
 end

+
 lemma env.empty_replace_sb: ∀ (b:sbool), freevar.env.empty⟦b⟧ = b
 := begin
  apply (and.elim_left env.empty_replace)
@ -530,18 +529,7 @@ lemma env.replace_sb_overflowchk_add: ∀
    sbitvec.overflow_chk @sbitvec.add sz2 nsw (η⟦v1⟧) (η⟦v2⟧)
 := begin
  intros, unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_add,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_add,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_add
-  }
+  cases nsw; simp, rw env.replace_sbv_of_int
 end

 lemma env.replace_sb_overflowchk_sub: ∀
@ -550,18 +538,7 @@ lemma env.replace_sb_overflowchk_sub: ∀
    sbitvec.overflow_chk @sbitvec.sub sz2 nsw (η⟦v1⟧) (η⟦v2⟧)
 := begin
  intros, unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_sub,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_sub,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_sub
-  }
+  cases nsw; simp, rw env.replace_sbv_of_int
 end

 lemma env.replace_sb_overflowchk_mul: ∀
@ -570,18 +547,7 @@ lemma env.replace_sb_overflowchk_mul: ∀
    sbitvec.overflow_chk @sbitvec.mul sz2 nsw (η⟦v1⟧) (η⟦v2⟧)
 := begin
  intros, unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_mul,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_mul,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_mul
-  }
+  cases nsw; simp, rw env.replace_sbv_of_int
 end

 lemma env.replace_sb_overflowchk_shl: ∀
@ -591,20 +557,9 @@ lemma env.replace_sb_overflowchk_shl: ∀
 := begin
  intros, unfold sbitvec.shl_overflow_chk,
  unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_shl,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int,
-    rw env.replace_sbv_urem, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_shl,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_shl,
-    rw env.replace_sbv_urem, rw env.replace_sbv_of_int
-  }
+  cases nsw; simp,
+  { repeat { rw env.replace_sbv_of_int }, tauto },
+  { rw env.replace_sbv_of_int, tauto }
 end

 -- irstate
@ -925,7 +880,7 @@ lemma env.add_b_replace_match: ∀ (η:freevar.env) n b,
  intros,
  unfold freevar.env.replace_sb,
  unfold freevar.env.add_b,
-  simp, unfold freevar.env.replace_sb._match_1
+  simp
 end

 lemma env.add_bv_replace_match: ∀ (η:freevar.env) n z sz,
@ -934,7 +889,7 @@ lemma env.add_bv_replace_match: ∀ (η:freevar.env) n z sz,
  intros,
  unfold freevar.env.replace_sbv,
  unfold freevar.env.add_bv,
-  simp, unfold freevar.env.replace_sbv._match_1
+  simp
 end

 lemma env.add_bv_replace_sb: ∀ (η:freevar.env) n n' z,
@ -1297,8 +1252,10 @@ lemma env.not_in_add_bv_irstate_comm: ∀ (η:freevar.env) (ss:irstate irsem_smt
      rw ss_snd_ih,
      cases ss_snd_hd with rn v,
      cases v with sz iv pv,
-      rw env.not_in_add_bv_valty_comm,
-      assumption
+      simp,
+      rw env.not_in_add_bv_bv_comm,
+      rw env.not_in_add_bv_b_comm,
+        assumption, assumption
    }
  }
 end
@ -1332,8 +1289,10 @@ lemma env.not_in_add_b_irstate_comm: ∀ (η:freevar.env) (ss:irstate irsem_smt)
      rw ss_snd_ih,
      cases ss_snd_hd with rn v,
      cases v with sz iv pv,
-      rw env.not_in_add_b_valty_comm,
-      assumption
+      simp,
+      rw env.not_in_add_b_bv_comm,
+      rw env.not_in_add_b_b_comm,
+        assumption, assumption
    }
  }
 end
--- a/src/spec/lemmas.lean
+++ b/src/spec/lemmas.lean
@ -185,7 +185,7 @@ lemma bvequiv_urem: ∀ (sz:size) (sb:sbitvec sz) eb
  intros,
  apply bv_equiv.urem, assumption, apply bvequiv_from_z,
  { cases sz, unfold_coes, simp, unfold uint_like.from_z, unfold bitvector.ne,
-    unfold bitvector.zero, unfold bitvector.of_int, simp,
+    unfold bitvector.of_int, simp,
    intros H, injection H, simp at h_1, rw nat.mod_pow2 at h_1,
    rw h_1 at sz_property, cases sz_property
  },
--- a/src/spec/openprog.lean
+++ b/src/spec/openprog.lean
@ -561,8 +561,8 @@ lemma step_replace: ∀ (ss:irstate_smt) (i:instruction)
      have HOPCOND' := apply_some HOPCOND,
      cases HOPCOND' with vopcond' HOPCOND',
      rw HOPCOND',
-      rw get_value_replace,
      unfold option.bind,
+      rw get_value_replace,
      
      cases vop1,
      { rw apply_none at HOP1, rw HOP1, unfold option.bind },