internlm/Lean-Github huggingface dataset:
Theorem: Nat.minus_plus_one
Proof state before:
case zero
h : zero > 0
⊢ zero - 1 + 1 = zero

case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝
Tactic:
simp at h
Proof state after:
case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝
Theorem: Nat.minus_plus_one
Proof state before:
case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝
Tactic:
rfl
Proof state after:
no goals
Theorem: transpose_remap_bound
Proof state before:
n m : ℕ
⊢ ∀ (i : ℕ), i < n * m → transpose_remap n m i < n * m
Tactic:
intro i h
Proof state after:
n m i : ℕ
h : i < n * m
⊢ transpose_remap n m i < n * m
Theorem: transpose_remap_bound
Proof state before:
n m i : ℕ
h : i < n * m
⊢ transpose_remap n m i < n * m
Tactic:
simp [transpose_remap]
Proof state after:
n m i : ℕ
h : i < n * m
⊢ m * (i % n) + i / n < n * m
Theorem: transpose_remap_bound
Proof state before:
n m i : ℕ
h : i < n * m
⊢ m * (i % n) + i / n < n * m
Tactic:
sorry
Proof state after:
no goals
Theorem: transpose_remap_involutive
Proof state before:
n m : ℕ
⊢ ∀ (i : ℕ), transpose_remap m n (transpose_remap n m i) = i
Tactic:
simp [transpose_remap, Function.comp]
Proof state after:
n m : ℕ
⊢ ∀ (i : ℕ), n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i
Theorem: transpose_remap_involutive
Proof state before:
n m : ℕ
⊢ ∀ (i : ℕ), n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i
Tactic:
intro i
Proof state after:
n m i : ℕ
⊢ n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i
Theorem: transpose_remap_involutive
Proof state before:
n m i : ℕ
⊢ n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i
Tactic:
sorry
Proof state after:
no goals
Theorem: Function.comp_assoc
Proof state before:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
⊢ (h ∘ g) ∘ f = h ∘ g ∘ f
Tactic:
funext x
Proof state after:
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
x : α
⊢ comp (h ∘ g) f x = comp h (g ∘ f) x
Theorem: Function.comp_assoc
Proof state before:
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
x : α
⊢ comp (h ∘ g) f x = comp h (g ∘ f) x
Tactic:
simp
Proof state after:
no goals
Theorem: transpose_involutive
Proof state before:
α n : ℕ
m : MLIR.AST.MLIRTy
⊢ ∀ (t : Matrix α n m), transpose (transpose t) = t
Tactic:
intro t
Proof state after:
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ transpose (transpose t) = t
Theorem: transpose_involutive
Proof state before:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ [α, n] = t.toTensor.shape

case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data
Tactic:
. rw [←dim_known_project_eq _ t.h_refines] <;> simp
Proof state after:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data
Theorem: transpose_involutive
Proof state before:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data
Tactic:
. simp [List.remap_remap]
  apply List.extF <;> simp
  simp [transpose_remap_involutive]
Proof state after:
no goals
Theorem: Fitree.id_map
Proof state before:
E : Type → Type
R : Type
t : Fitree E R
⊢ id <$> t = t
Tactic:
simp [Functor.map]
Proof state after:
E : Type → Type
R : Type
t : Fitree E R
⊢ bind t (ret ∘ id) = t
Theorem: Fitree.id_map
Proof state before:
E : Type → Type
R : Type
t : Fitree E R
⊢ bind t (ret ∘ id) = t
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.id_map
Proof state before:
case Ret
E : Type → Type
R : Type
r✝ : R
⊢ bind (Ret r✝) (ret ∘ id) = Ret r✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.id_map
Proof state before:
case Vis
E : Type → Type
R T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝), bind (k✝ a) (ret ∘ id) = k✝ a
⊢ bind (Vis e✝ k✝) (ret ∘ id) = Vis e✝ k✝
Tactic:
simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.comp_map
Proof state before:
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
t : Fitree E R₁
⊢ (g ∘ f) <$> t = g <$> f <$> t
Tactic:
simp [Functor.map]
Proof state after:
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
t : Fitree E R₁
⊢ bind t (ret ∘ g ∘ f) = bind t fun x => ret (g (f x))
Theorem: Fitree.comp_map
Proof state before:
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
t : Fitree E R₁
⊢ bind t (ret ∘ g ∘ f) = bind t fun x => ret (g (f x))
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.comp_map
Proof state before:
case Ret
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
r✝ : R₁
⊢ bind (Ret r✝) (ret ∘ g ∘ f) = bind (Ret r✝) fun x => ret (g (f x))
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.comp_map
Proof state before:
case Vis
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), bind (k✝ a) (ret ∘ g ∘ f) = bind (k✝ a) fun x => ret (g (f x))
⊢ bind (Vis e✝ k✝) (ret ∘ g ∘ f) = bind (Vis e✝ k✝) fun x => ret (g (f x))
Tactic:
simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.seqLeft_eq
Proof state before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (SeqLeft.seqLeft t₁ fun x => t₂) = Seq.seq (Function.const R₂ <$> t₁) fun x => t₂
Tactic:
simp [SeqLeft.seqLeft, Seq.seq]
Proof state after:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> t₁) fun y => bind t₂ (ret ∘ y)
Theorem: Fitree.seqLeft_eq
Proof state before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> t₁) fun y => bind t₂ (ret ∘ y)
Tactic:
induction t₁ with
| Ret _ => rfl
| Vis _ _ ih => simp [bind]; funext _; simp [ih]; sorry
Proof state after:
no goals
Theorem: Fitree.seqLeft_eq
Proof state before:
case Ret
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
r✝ : R₁
⊢ (bind (Ret r✝) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> Ret r✝) fun y => bind t₂ (ret ∘ y)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.seqLeft_eq
Proof state before:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (bind (Vis e✝ k✝) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> Vis e✝ k✝) fun y => bind t₂ (ret ∘ y)
Tactic:
simp [bind]
Proof state after:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun a => bind t₂ fun x => ret a) = fun r =>
    bind (k✝ r) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Theorem: Fitree.seqLeft_eq
Proof state before:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun a => bind t₂ fun x => ret a) = fun r =>
    bind (k✝ r) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Tactic:
funext _
Proof state after:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun a => bind t₂ fun x => ret a) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Theorem: Fitree.seqLeft_eq
Proof state before:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun a => bind t₂ fun x => ret a) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Tactic:
simp [ih]
Proof state after:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₂ <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) =
    bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Theorem: Fitree.seqLeft_eq
Proof state before:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₂ <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) =
    bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Tactic:
sorry
Proof state after:
no goals
Theorem: Fitree.seqRight_eq
Proof state before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (SeqRight.seqRight t₁ fun x => t₂) = Seq.seq (Function.const R₁ id <$> t₁) fun x => t₂
Tactic:
simp [SeqRight.seqRight, Seq.seq]
Proof state after:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun x => t₂) = bind (Function.const R₁ id <$> t₁) fun y => bind t₂ (ret ∘ y)
Theorem: Fitree.seqRight_eq
Proof state before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun x => t₂) = bind (Function.const R₁ id <$> t₁) fun y => bind t₂ (ret ∘ y)
Tactic:
induction t₁ with
| Ret _ =>
  simp [Function.const, Function.comp, bind]
| Vis _ _ ih =>
  simp [bind]; funext _; simp [ih]; sorry
Proof state after:
no goals
Theorem: Fitree.seqRight_eq
Proof state before:
case Ret
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
r✝ : R₁
⊢ (bind (Ret r✝) fun x => t₂) = bind (Function.const R₁ id <$> Ret r✝) fun y => bind t₂ (ret ∘ y)
Tactic:
simp [Function.const, Function.comp, bind]
Proof state after:
no goals
Theorem: Fitree.seqRight_eq
Proof state before:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (bind (Vis e✝ k✝) fun x => t₂) = bind (Function.const R₁ id <$> Vis e✝ k✝) fun y => bind t₂ (ret ∘ y)
Tactic:
simp [bind]
Proof state after:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun x => t₂) = fun r => bind (k✝ r) fun x => bind t₂ (ret ∘ id)
Theorem: Fitree.seqRight_eq
Proof state before:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun x => t₂) = fun r => bind (k✝ r) fun x => bind t₂ (ret ∘ id)
Tactic:
funext _
Proof state after:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun x => t₂) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)
Theorem: Fitree.seqRight_eq
Proof state before:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun x => t₂) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)
Tactic:
simp [ih]
Proof state after:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₁ id <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)
Theorem: Fitree.seqRight_eq
Proof state before:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₁ id <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)
Tactic:
sorry
Proof state after:
no goals
Theorem: Fitree.seq_assoc
Proof state before:
E : Type → Type
R₁ R₂ R₃ : Type
t₁ : Fitree E R₁
t₂ : Fitree E (R₁ → R₂)
t₃ : Fitree E (R₂ → R₃)
⊢ (Seq.seq t₃ fun x => Seq.seq t₂ fun x => t₁) = Seq.seq (Seq.seq (Function.comp <$> t₃) fun x => t₂) fun x => t₁
Tactic:
sorry
Proof state after:
no goals
Theorem: Fitree.bind_assoc
Proof state before:
E : Type → Type
R₁ R₂ R₃ : Type
t : Fitree E R₁
k₁ : R₁ → Fitree E R₂
k₂ : R₂ → Fitree E R₃
⊢ bind (bind t k₁) k₂ = bind t fun x => bind (k₁ x) k₂
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind];
Proof state after:
no goals
Theorem: Fitree.bind_assoc
Proof state before:
case Ret
E : Type → Type
R₁ R₂ R₃ : Type
k₁ : R₁ → Fitree E R₂
k₂ : R₂ → Fitree E R₃
r✝ : R₁
⊢ bind (bind (Ret r✝) k₁) k₂ = bind (Ret r✝) fun x => bind (k₁ x) k₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.bind_assoc
Proof state before:
case Vis
E : Type → Type
R₁ R₂ R₃ : Type
k₁ : R₁ → Fitree E R₂
k₂ : R₂ → Fitree E R₃
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), bind (bind (k✝ a) k₁) k₂ = bind (k✝ a) fun x => bind (k₁ x) k₂
⊢ bind (bind (Vis e✝ k✝) k₁) k₂ = bind (Vis e✝ k✝) fun x => bind (k₁ x) k₂
Tactic:
simp [bind]
Proof state after:
no goals
Theorem: tst3
Proof state before:
p q : Prop
⊢ p → q → p
Tactic:
intros h1 h2
Proof state after:
p q : Prop
h1 : p
h2 : q
⊢ p
Theorem: tst3
Proof state before:
p q : Prop
h1 : p
h2 : q
⊢ p
Tactic:
assumption
Proof state after:
no goals
Theorem: FinInt.mod2_ge
Proof state before:
a : ℤ
n : ℕ
⊢ mod2 a n ≥ 0
Tactic:
simp [mod2]
Proof state after:
a : ℤ
n : ℕ
⊢ 0 ≤ a % 2 ^ n
Theorem: FinInt.mod2_ge
Proof state before:
a : ℤ
n : ℕ
⊢ 0 ≤ a % 2 ^ n
Tactic:
apply Int.mod_ge
Proof state after:
case a
a : ℤ
n : ℕ
⊢ a ≥ 0
Theorem: FinInt.mod2_ge
Proof state before:
case a
a : ℤ
n : ℕ
⊢ a ≥ 0
Tactic:
have h := Int.ge_add_ge_right (2^n) (@Int.mod_ge_neg a (2^n))
Proof state after:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ -2 ^ n + 2 ^ n
⊢ a ≥ 0
Theorem: FinInt.mod2_ge
Proof state before:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ -2 ^ n + 2 ^ n
⊢ a ≥ 0
Tactic:
rw [Int.add_left_neg] at h
Proof state after:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ 0
⊢ a ≥ 0
Theorem: FinInt.mod2_ge
Proof state before:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ 0
⊢ a ≥ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.mod2_lt
Proof state before:
a : ℤ
n : ℕ
⊢ mod2 a n < 2 ^ n
Tactic:
simp [mod2]
Proof state after:
a : ℤ
n : ℕ
⊢ a % 2 ^ n < 2 ^ n
Theorem: FinInt.mod2_lt
Proof state before:
a : ℤ
n : ℕ
⊢ a % 2 ^ n < 2 ^ n
Tactic:
apply Int.mod_lt Int.two_pow_pos
Proof state after:
no goals
Theorem: FinInt.mod2_idem
Proof state before:
n : ℕ
a : ℤ
⊢ a ≥ 0 ∧ a < 2 ^ n → mod2 a n = a
Tactic:
intros h
Proof state after:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ mod2 a n = a
Theorem: FinInt.mod2_idem
Proof state before:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ mod2 a n = a
Tactic:
simp [mod2]
Proof state after:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ a % 2 ^ n = a
Theorem: FinInt.mod2_idem
Proof state before:
n : ℕ
a : ℤ
h : a ≥ 0 ∧ a < 2 ^ n
⊢ a % 2 ^ n = a
Tactic:
simp [Int.mod_bounds _ h.1 h.2]
Proof state after:
no goals
Theorem: FinInt.mod2_fequal
Proof state before:
x y : ℤ
n : ℕ
⊢ x = y → mod2 x n = mod2 y n
Tactic:
intros h
Proof state after:
x y : ℤ
n : ℕ
h : x = y
⊢ mod2 x n = mod2 y n
Theorem: FinInt.mod2_fequal
Proof state before:
x y : ℤ
n : ℕ
h : x = y
⊢ mod2 x n = mod2 y n
Tactic:
simp [h]
Proof state after:
no goals
Theorem: FinInt.mod2_zero
Proof state before:
n : ℕ
⊢ mod2 0 n = 0
Tactic:
simp [mod2]
Proof state after:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0
Theorem: FinInt.mod2_zero
Proof state before:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0
Tactic:
simp [Int.emod_self]
Proof state after:
no goals
Theorem: FinInt.mod2_exp_n
Proof state before:
n : ℕ
⊢ mod2 (2 ^ n) n = 0
Tactic:
simp [mod2]
Proof state after:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0
Theorem: FinInt.mod2_exp_n
Proof state before:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0
Tactic:
simp [Int.emod_self]
Proof state after:
no goals
Theorem: FinInt.mod2_add_left
Proof state before:
n : ℕ
x : ℤ
⊢ mod2 (2 ^ n + x) n = mod2 x n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.mod2_add_right
Proof state before:
x : ℤ
n : ℕ
⊢ mod2 (x + 2 ^ n) n = mod2 x n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.smod2_ge
Proof state before:
a : ℤ
n : ℕ
⊢ smod2 a n ≥ -2 ^ n
Tactic:
simp [smod2]
Proof state after:
a : ℤ
n : ℕ
⊢ -2 ^ n ≤ if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)
Theorem: FinInt.smod2_ge
Proof state before:
a : ℤ
n : ℕ
⊢ -2 ^ n ≤ if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)
Tactic:
split
Proof state after:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1) - 2 ^ (n + 1)

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)
Theorem: FinInt.smod2_ge
Proof state before:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1) - 2 ^ (n + 1)

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)
Tactic:
. sorry_arith
Proof state after:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)
Theorem: FinInt.smod2_ge
Proof state before:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)
Tactic:
. apply Int.ge_trans 0 mod2_ge (Int.zero_ge_neg Int.two_pow_ge)
Proof state after:
no goals
Theorem: FinInt.smod2_lt
Proof state before:
a : ℤ
n : ℕ
⊢ smod2 a n < 2 ^ n
Tactic:
simp [smod2]
Proof state after:
a : ℤ
n : ℕ
⊢ (if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)) < 2 ^ n
Theorem: FinInt.smod2_lt
Proof state before:
a : ℤ
n : ℕ
⊢ (if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)) < 2 ^ n
Tactic:
split
Proof state after:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) - 2 ^ (n + 1) < 2 ^ n

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n
Theorem: FinInt.smod2_lt
Proof state before:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) - 2 ^ (n + 1) < 2 ^ n

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n
Tactic:
. sorry_arith
Proof state after:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n
Theorem: FinInt.smod2_lt
Proof state before:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ mod2 a (n + 1) < 2 ^ n
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.smod2_idem
Proof state before:
n : ℕ
a : ℤ
⊢ a ≥ -2 ^ n ∧ a < 2 ^ n → smod2 a n = a
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.smod2_as_mod2
Proof state before:
a : ℤ
n : ℕ
⊢ smod2 a n = mod2 (a + 2 ^ n) (n + 1) - 2 ^ n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.cong2_to_eq
Proof state before:
a b : ℤ
n : ℕ
⊢ a ≡ b [2^n] → a ≥ 0 ∧ a < 2 ^ n → b ≥ 0 ∧ b < 2 ^ n → a = b
Tactic:
intros h ha hb
Proof state after:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ a = b
Theorem: FinInt.cong2_to_eq
Proof state before:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ a = b
Tactic:
rw [←mod2_idem ha, ←mod2_idem hb]
Proof state after:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ mod2 a n = mod2 b n
Theorem: FinInt.cong2_to_eq
Proof state before:
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ mod2 a n = mod2 b n
Tactic:
assumption
Proof state after:
no goals
Theorem: FinInt.scong2_to_eq
Proof state before:
a b : ℤ
n : ℕ
⊢ a ≡ b [±2^n] → a ≥ -2 ^ n ∧ a < 2 ^ n → b ≥ -2 ^ n ∧ b < 2 ^ n → a = b
Tactic:
intros h ha hb
Proof state after:
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ a = b
Theorem: FinInt.scong2_to_eq
Proof state before:
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ a = b
Tactic:
rw [←smod2_idem ha, ←smod2_idem hb]
Proof state after:
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ smod2 a n = smod2 b n
Theorem: FinInt.scong2_to_eq
Proof state before:
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ smod2 a n = smod2 b n
Tactic:
assumption
Proof state after:
no goals
Theorem: FinInt.mod2_add_l
Proof state before:
a : ℤ
n : ℕ
b : ℤ
⊢ mod2 (mod2 a n + b) n = mod2 (a + b) n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.mod2_add_r
Proof state before:
a b : ℤ
n : ℕ
⊢ mod2 (a + mod2 b n) n = mod2 (a + b) n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.mod2_neg
Proof state before:
a : ℤ
n : ℕ
⊢ mod2 (-mod2 a n) n = mod2 (-a) n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.mod2_sub_r
Proof state before:
a b : ℤ
n : ℕ
⊢ mod2 (a - mod2 b n) n = mod2 (a - b) n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.mod2_sub_l
Proof state before:
a : ℤ
n : ℕ
b : ℤ
⊢ mod2 (mod2 a n - b) n = mod2 (a - b) n
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.cong2_mod2_right
Proof state before:
n : ℕ
a b : ℤ
⊢ a ≡ b [2^n] → a ≡ mod2 b n [2^n]
Tactic:
simp [cong2, mod2_idem mod2_bounds]
Proof state after:
no goals
Theorem: FinInt.cong2_mod2_left
Proof state before:
n : ℕ
a b : ℤ
⊢ a ≡ b [2^n] → mod2 a n ≡ b [2^n]
Tactic:
simp [cong2, mod2_idem mod2_bounds]
Proof state after:
no goals
Theorem: FinInt.toUint_ge
Proof state before:
sz : ℕ
n : FinInt sz
⊢ toUint n ≥ 0
Tactic:
revert n
Proof state after:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n ≥ 0