Predicate support

SSA/Experimental/Bits/Defs.lean

@@ -53,20 +53,20 @@ so eval requires us to give a value for each possible variable.
 -/
 def Term.eval (t : Term) (vars : Nat → BitStream) : BitStream :=
   match t with
-  | var n     => vars n
-  | zero      => BitStream.zero
-  | one       => BitStream.one
-  | negOne    => BitStream.negOne
-  | and t₁ t₂ => (t₁.eval vars) &&& (t₂.eval vars)
-  | or t₁ t₂  => (t₁.eval vars) ||| (t₂.eval vars)
-  | xor t₁ t₂ => (t₁.eval vars) ^^^ (t₂.eval vars)
-  | not t     => ~~~(t.eval vars)
-  | ls b t    => (Term.eval t vars).concat b
-  | add t₁ t₂ => (Term.eval t₁ vars) + (Term.eval t₂ vars)
-  | sub t₁ t₂ => (Term.eval t₁ vars) - (Term.eval t₂ vars)
-  | neg t     => -(Term.eval t vars)
-  | incr t    => BitStream.incr (Term.eval t vars)
-  | decr t    => BitStream.decr (Term.eval t vars)
+  | var n       => vars n
+  | zero        => BitStream.zero
+  | one         => BitStream.one
+  | negOne      => BitStream.negOne
+  | and t₁ t₂   => (t₁.eval vars) &&& (t₂.eval vars)
+  | or t₁ t₂    => (t₁.eval vars) ||| (t₂.eval vars)
+  | xor t₁ t₂   => (t₁.eval vars) ^^^ (t₂.eval vars)
+  | not t       => ~~~(t.eval vars)
+  | ls b t      => (Term.eval t vars).concat b
+  | add t₁ t₂   => (Term.eval t₁ vars) + (Term.eval t₂ vars)
+  | sub t₁ t₂   => (Term.eval t₁ vars) - (Term.eval t₂ vars)
+  | neg t       => -(Term.eval t vars)
+  | incr t      => BitStream.incr (Term.eval t vars)
+  | decr t      => BitStream.decr (Term.eval t vars)
 
 instance : Add Term := ⟨add⟩
 instance : Sub Term := ⟨sub⟩
@@ -130,6 +130,6 @@ and only require that many bitstream values to be given in `vars`.
       let x₁ := t₁.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
       let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i))
       x₁ - x₂
-  | neg t  => -(Term.evalFin t vars)
-  | incr t => BitStream.incr (Term.evalFin t vars)
-  | decr t => BitStream.decr (Term.evalFin t vars)
+  | neg t       => -(Term.evalFin t vars)
+  | incr t      => BitStream.incr (Term.evalFin t vars)
+  | decr t      => BitStream.decr (Term.evalFin t vars)

SSA/Experimental/Bits/Fast/BitStream.lean

@@ -98,6 +98,45 @@ section Lemmas
 theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y := by
   funext i; exact h i
 
+/--
+The field projection `.1` distributes over function composition, so we can compute
+the first field of the result of the composition by repeatedly composing the first projection.
+-/
+theorem compose_first {α: Type u₁} (i : Nat) (a : α) 
+    (f : α → α × Bool) : 
+    (f ((Prod.fst ∘ f)^[i] a)).1 = (Prod.fst ∘ f)^[i] (f a).1 :=
+  match i with
+    | 0 => by simp
+    | i + 1 => by simp [compose_first i ((f a).1) f]
+
+/--
+Coinduction principle for `corec`.
+To show that `corec f a = corec g b`,
+we must show that:
+- The relation `R a b` is inhabited ["base case"]
+- Given that `R a b` holds, then `R (f a) (g b)` holds [coinductive case]
+-/
+theorem corec_eq_corec {a : α} {b : β} {f g}
+    (R : α → β → Prop)
+    (thing : R a b)
+    (h : ∀ a b, R a b →
+          let x := f a
+          let y := g b
+          R x.fst y.fst ∧ x.snd = y.snd) :
+    corec f a = corec g b := by
+  ext i
+  have lem : R ((Prod.fst ∘ f)^[i] (f a).1) ((Prod.fst ∘ g)^[i] (g b).1) ∧ corec f a i = corec g b i := by
+    induction' i with i ih
+    <;> simp only [Function.iterate_succ, Function.comp_apply, corec]
+    · apply h
+      exact thing
+    · have m := h ((Prod.fst ∘ f)^[i] (f a).1) ((Prod.fst ∘ g)^[i] (g b).1) (ih.1)
+      cases' m with l r
+      rw [r, ← compose_first, ← @compose_first β]
+      simp [l]
+  cases lem
+  assumption
+
 end Lemmas
 
 end Basic
@@ -276,6 +315,16 @@ instance : Add BitStream := ⟨add⟩
 instance : Neg BitStream := ⟨neg⟩
 instance : Sub BitStream := ⟨sub⟩
 
+/-- `repeatBit xs` will repeat the first bit of `xs` which is `true`.
+That is, it will be all-zeros iff `xs` is all-zeroes,
+otherwise, there's some number `k` so that after dropping the `k` least
+significant bits, `repeatBit xs` is all-ones. -/
+def repeatBit (xs : BitStream) : BitStream :=
+  corec (b := (false, xs)) fun (carry, xs) =>
+    let carry := carry || xs 0
+    let xs := xs.tail
+    ((carry, xs), carry)
+
 /-!
 TODO: We should define addition and `carry` in terms of `mapAccum`.
 For example:

SSA/Experimental/Bits/Fast/Decide.lean

@@ -1,5 +1,5 @@
 import SSA.Experimental.Bits.Fast.FiniteStateMachine
-import SSA.Experimental.Bits.Lemmas
+import SSA.Experimental.Bits.Fast.Lemmas
 
 instance (t₁ t₂ : Term) : Decidable (t₁.eval = t₂.eval) :=
   decidable_of_iff
@@ -33,96 +33,110 @@ example : ((and x y) + (or x y)).eval = (x + y).eval := by
 example : ((or x y) - (xor x y)).eval = (and x y).eval := by
   native_decide
 
+
+/-
+Note that we use `#eval!` instead of `#eval`, since our
+proof of `decide` currently contains a `sorry`. We should elminate the `sorry`,
+and then switch to `#eval`.
+-/
+
+/--
+info: 'Decidable.decide' does not depend on any axioms
+---
+info: 'decide' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
+-/
+#guard_msgs in #print axioms decide
+
 /-- info: true -/
-#guard_msgs in #eval decide (x + -x) 0
+#guard_msgs in #eval! decide (x + -x) 0
 
 /-- info: true -/
-#guard_msgs in #eval decide (incr x) (x + 1)
+#guard_msgs in #eval! decide (incr x) (x + 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (decr x) (x - 1)
+#guard_msgs in #eval! decide (decr x) (x - 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + -y) (x - y)
+#guard_msgs in #eval! decide (x + -y) (x - y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + 0) (var 0)
+#guard_msgs in #eval! decide (x + 0) (var 0)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) (y + x)
+#guard_msgs in #eval! decide (x + y) (y + x)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + (y + z)) (x + y + z)
+#guard_msgs in #eval! decide (x + (y + z)) (x + y + z)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - x) 0
+#guard_msgs in #eval! decide (x - x) 0
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + 0) x
+#guard_msgs in #eval! decide (x + 0) x
 
 /-- info: true -/
-#guard_msgs in #eval decide (0 + x) x
+#guard_msgs in #eval! decide (0 + x) x
 
 /-- info: true -/
-#guard_msgs in #eval decide (-x) (not x).incr
+#guard_msgs in #eval! decide (-x) (not x).incr
 
 /-- info: true -/
-#guard_msgs in #eval decide (-x) (not x.decr)
+#guard_msgs in #eval! decide (-x) (not x.decr)
 
 /-- info: true -/
-#guard_msgs in #eval decide (not x) (-x).decr
+#guard_msgs in #eval! decide (not x) (-x).decr
 
 /-- info: true -/
-#guard_msgs in #eval decide (-not x) (x + 1)
+#guard_msgs in #eval! decide (-not x) (x + 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) (x - not y - 1)
+#guard_msgs in #eval! decide (x + y) (x - not y - 1)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) ((xor x y) + (and x y).ls false)
+#guard_msgs in #eval! decide (x + y) ((xor x y) + (and x y).ls false)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) (or x y + and x y)
+#guard_msgs in #eval! decide (x + y) (or x y + and x y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x + y) ((or x y).ls false - (xor x y))
+#guard_msgs in #eval! decide (x + y) ((or x y).ls false - (xor x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) (x + not y).incr
+#guard_msgs in #eval! decide (x - y) (x + not y).incr
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) (xor x y - (and (not x) y).ls false)
+#guard_msgs in #eval! decide (x - y) (xor x y - (and (not x) y).ls false)
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) (and x (not y) - (and (not x) y))
+#guard_msgs in #eval! decide (x - y) (and x (not y) - (and (not x) y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (x - y) ((and x (not y)).ls false - (xor x y))
+#guard_msgs in #eval! decide (x - y) ((and x (not y)).ls false - (xor x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (xor x y) ((or x y) - (and x y))
+#guard_msgs in #eval! decide (xor x y) ((or x y) - (and x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (and x (not y)) (or x y - y)
+#guard_msgs in #eval! decide (and x (not y)) (or x y - y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (and x (not y)) (x - and x y)
+#guard_msgs in #eval! decide (and x (not y)) (x - and x y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (x - y)) (y - x).decr
+#guard_msgs in #eval! decide (not (x - y)) (y - x).decr
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (x - y)) (not x + y)
+#guard_msgs in #eval! decide (not (x - y)) (not x + y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (xor x y)) (and x y - (or x y)).decr
+#guard_msgs in #eval! decide (not (xor x y)) (and x y - (or x y)).decr
 
 /-- info: true -/
-#guard_msgs in #eval decide (not (xor x y)) (and x y + not (or x y))
+#guard_msgs in #eval! decide (not (xor x y)) (and x y + not (or x y))
 
 /-- info: true -/
-#guard_msgs in #eval decide (or x y) (and x (not y) + y)
+#guard_msgs in #eval! decide (or x y) (and x (not y) + y)
 
 /-- info: true -/
-#guard_msgs in #eval decide (and x y) (or (not x) y - not x)
+#guard_msgs in #eval! decide (and x y) (or (not x) y - not x)
 end testDecide