summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Scalar.lean
blob: 8793713b245f5a01e0783dfe9a5941d6c7b83d07 (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
import Base.Arith.Int
import Base.Primitives.Scalar

/- Automation for scalars - TODO: not sure it is worth having two files (Int.lean and Scalar.lean) -/
namespace Arith

open Lean Lean.Elab Lean.Meta
open Primitives

def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
  Tactic.withMainContext do
  -- Inroduce the bounds for the isize/usize types
  let add (e : Expr) : Tactic.TacticM Unit := do
    let ty  inferType e
    let _  Utils.addDeclTac ( Utils.mkFreshAnonPropUserName) e ty (asLet := false)
  add ( mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
  add ( mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
  add ( mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
  -- Reveal the concrete bounds, simplify calls to [ofInt]
  Utils.simpAt true {}
               -- Unfoldings
               [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
                ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
                ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
                ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
                ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max,
                ``Usize.min
                ]
                -- Simp lemmas
                [``Scalar.ofInt_val_eq, ``Scalar.neq_to_neq_val,
                 ``Scalar.lt_equiv, ``Scalar.le_equiv, ``Scalar.eq_equiv]
                -- Hypotheses
                [] .wildcard

elab "scalar_tac_preprocess" : tactic =>
  intTacPreprocess scalarTacExtraPreprocess

-- A tactic to solve linear arithmetic goals in the presence of scalars
def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
  intTac "scalar_tac" splitGoalConjs scalarTacExtraPreprocess

elab "scalar_tac" : tactic =>
  scalarTac false

-- For termination proofs
syntax "scalar_decr_tac" : tactic
macro_rules
  | `(tactic| scalar_decr_tac) =>
    `(tactic|
      simp_wf;
      -- TODO: don't use a macro (namespace problems)
      (first | apply Arith.to_int_to_nat_lt
             | apply Arith.to_int_sub_to_nat_lt) <;>
      simp_all <;> scalar_tac)

instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
  -- prop_ty is inferred
  prop := λ x => And.intro x.hmin x.hmax

example (x y : U32) : x.val  Scalar.max ScalarTy.U32 := by
  intro_has_int_prop_instances
  simp [*]

example (x y : U32) : x.val  Scalar.max ScalarTy.U32 := by
  scalar_tac

-- Checking that we explore the goal *and* projectors correctly
example (x : U32 × U32) : 0  x.fst.val := by
  scalar_tac

-- Checking that we properly handle [ofInt]
example : U32.ofInt 1  U32.max := by
  scalar_tac

example (x : Int) (h0 : 0  x) (h1 : x  U32.max) :
  U32.ofIntCore x (by constructor <;> scalar_tac)  U32.max := by
  scalar_tac

-- Not equal
example (x : U32) (h0 : ¬ x = U32.ofInt 0) : 0 < x.val := by
  scalar_tac

/- See this: https://aeneas-verif.zulipchat.com/#narrow/stream/349819-general/topic/U64.20trouble/near/444049757

   We solved it by removing the instance `OfNat` for `Scalar`.
   Note however that we could also solve it with a simplification lemma.
   However, after testing, we noticed we could only apply such a lemma with
   the rewriting tactic (not the simplifier), probably because of the use
   of typeclasses. -/
example {u: U64} (h1: (u : Int) < 2): (u : Int) = 0  (u : Int) = 1 := by
  scalar_tac

end Arith