Binary-4/LtReasoning.agda at master · mechvel/Binary-4 · 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
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
108
109
110
111
112
113
114
115
116
117
118
119

-- This is by  Ulf Norell:
-- a suport for reasoning with inequalities.

-- "In response to https://lists.chalmers.se/pipermail/agda/2017/009872.html "


module LtReasoning where

open import Agda.Builtin.Equality

infix 0 case_of_
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

-- Equality reasoning --

module InequalityReasoning {a b} {A : Set a}
              (_<_ : A → A → Set b)
              (_≤_ : A → A → Set b)
              (leq-refl     : ∀ {x y}   → x ≡ y → x ≤ y)
              (lt-trans     : ∀ {x y z} → x < y → y < z → x < z)
              (leq-trans    : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z)
              (lt/leq-trans : ∀ {x y z} → x < y → y ≤ z → x < z)
              (leq/lt-trans : ∀ {x y z} → x ≤ y → y < z → x < z)
  where

  data _≲_ (x y : A) : Set b where
    strict    : x < y → x ≲ y
    nonstrict : x ≤ y → x ≲ y

  module _ {x y : A} where
    ⟦_⟧ : x ≲ y → Set b
    ⟦ strict    _ ⟧ = x < y
    ⟦ nonstrict _ ⟧ = x ≤ y

    infix -1 begin_
    begin_ : (p : x ≲ y) → ⟦ p ⟧
    begin strict    p = p
    begin nonstrict p = p

  infixr 0 eqReasoningStep ltReasoningStep leqReasoningStep
  infix  1 _∎

  syntax eqReasoningStep x q p = x ≡[ p ] q
  eqReasoningStep : ∀ (x : A) {y z} → y ≲ z → x ≡ y → x ≲ z
  x ≡[ x=y ] strict    y<z = strict    (case x=y of λ where refl → y<z)
  x ≡[ x=y ] nonstrict y≤z = nonstrict (case x=y of λ where refl → y≤z)
    -- ^ Note: don't match on the proof here, we need to decide strict vs
    -- nonstrict for neutral proofs

  syntax ltReasoningStep x q p = x <[ p ] q
  ltReasoningStep : ∀ (x : A) {y z} → y ≲ z → x < y → x ≲ z
  x <[ x<y ] strict    y<z = strict (lt-trans x<y y<z)
  x <[ x<y ] nonstrict y≤z = strict (lt/leq-trans x<y y≤z)

  syntax leqReasoningStep x q p = x ≤[ p ] q
  leqReasoningStep : ∀ (x : A) {y z} → y ≲ z → x ≤ y → x ≲ z
  x ≤[ x≤y ] strict    y<z = strict    (leq/lt-trans x≤y y<z)
  x ≤[ x≤y ] nonstrict y≤z = nonstrict (leq-trans x≤y y≤z)

  _∎ : ∀ (x : A) → x ≲ x
  x ∎ = nonstrict (leq-refl refl)


-- Example -----------------------------------

{-
  Bin : Set
  0# 0bs1 0bs'1 bs1 bs'1 2bin : Bin
  _*2 : Bin → Bin
  _+_ _*_ : Bin → Bin → Bin
  _<_ _≤_ : Bin → Bin → Set

  leq-refl : ∀ {x y} → x ≡ y → x ≤ y
  lt-trans : ∀ {x y z} → x < y → y < z → x < z
  leq-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
  lt/leq-trans : ∀ {x y z} → x < y → y ≤ z → x < z
  leq/lt-trans : ∀ {x y z} → x ≤ y → y < z → x < z


infix 7 _*2
infixl 7 _*_
infixl 6 _+_
infix 3 _<_ _≤_

open InequalityReasoning _<_ _≤_ leq-refl lt-trans leq-trans lt/leq-trans
                                                             leq/lt-trans

  step-1 : 0bs1 ≡ bs1 * 2bin
  step-2 : bs1 * 2bin < bs'1 * 2bin
  step-3 : bs'1 * 2bin ≡ bs'1 *2
  step-4 : bs'1 *2 ≡ 0# + 0bs'1

goal : 0bs1 < 0# + 0bs'1
goal =
  begin 0bs1           ≡[ step-1 ]
        bs1 * 2bin     <[ step-2 ]
        bs'1 * 2bin    ≡[ step-3 ]
        bs'1 *2        ≡[ step-4 ]
        0# + 0bs'1
  ∎

goal' : 0bs1 < 0# + 0bs'1
goal' =
  begin 0bs1           ≤[ leq-refl step-1 ]
        bs1 * 2bin     <[ step-2 ]
        bs'1 * 2bin    ≤[ leq-refl step-3 ]
        bs'1 *2        ≡[ step-4 ]
        0# + 0bs'1
  ∎

test : bs'1 * 2bin ≤ 0# + 0bs'1
test =
  begin bs'1 * 2bin  ≤[ leq-refl step-3 ]
        bs'1 *2      ≡[ step-4 ]
        0# + 0bs'1
  ∎
-}