chore: style
Use `·` instead of `.` for structuring tactics.
This commit is contained in:
Leonardo de Moura
parent
ddf93d2f8a
commit
5caf1bc692
16 changed files with 106 additions and 106 deletions
|
|
@ -11,13 +11,13 @@ namespace Array
|
|||
|
||||
theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a.get ⟨j, high⟩ = b.get ⟨j, hsz ▸ high⟩ := by
|
||||
by_cases h : i < a.size
|
||||
. unfold Array.isEqvAux at heqv
|
||||
· unfold Array.isEqvAux at heqv
|
||||
simp [h] at heqv
|
||||
have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
|
||||
by_cases heq : i = j
|
||||
. subst heq; exact heqv.1
|
||||
. exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
|
||||
. have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
|
||||
· subst heq; exact heqv.1
|
||||
· exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
|
||||
· have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
|
||||
subst heq
|
||||
exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
|
||||
termination_by _ => a.size - i
|
||||
|
|
|
|||
|
|
@ -33,10 +33,10 @@ theorem sizeOf_lt_of_mem [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈
|
|||
let rec aux (j : Nat) (h : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true) : sizeOf a < sizeOf as := by
|
||||
unfold anyM.loop at h
|
||||
split at h
|
||||
. simp [Bind.bind, pure] at h; split at h
|
||||
· simp [Bind.bind, pure] at h; split at h
|
||||
next he => subst a; apply sizeOf_get_lt
|
||||
next => have ih := aux (j+1) h; assumption
|
||||
. contradiction
|
||||
· contradiction
|
||||
apply aux 0 h
|
||||
termination_by aux j _ => as.size - j
|
||||
|
||||
|
|
|
|||
|
|
@ -356,26 +356,26 @@ theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
|
|||
split <;> simp at h <;> try assumption
|
||||
rename_i k₁ v₁ m₁ k₂ v₂ m₂
|
||||
by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
|
||||
. apply ih; simp [denote_eq] at h |-; assumption
|
||||
. by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
|
||||
. apply ih; simp [denote_eq] at h |-; assumption
|
||||
. have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
· apply ih; simp [denote_eq] at h |-; assumption
|
||||
· by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
|
||||
· apply ih; simp [denote_eq] at h |-; assumption
|
||||
· have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
|
||||
. apply ih
|
||||
· apply ih
|
||||
simp [denote_eq] at h |-
|
||||
have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
|
||||
apply Eq.symm
|
||||
apply Nat.sub_eq_of_eq_add
|
||||
simp [h]
|
||||
. by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
|
||||
. apply ih
|
||||
· by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
|
||||
· apply ih
|
||||
simp [denote_eq] at h |-
|
||||
have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
|
||||
apply Nat.sub_eq_of_eq_add
|
||||
simp [h]
|
||||
. have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
· have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
apply ih
|
||||
simp [denote_eq] at h |-
|
||||
rw [← Nat.add_assoc, ← Nat.add_assoc] at h
|
||||
|
|
@ -390,25 +390,25 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
|
|||
split at h <;> simp <;> try assumption
|
||||
rename_i k₁ v₁ m₁ k₂ v₂ m₂
|
||||
by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
|
||||
. have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
|
||||
. by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
|
||||
. have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
|
||||
. have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
· have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
|
||||
· by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
|
||||
· have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
|
||||
· have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
|
||||
. have ih := ih (h := h); simp [denote_eq] at ih ⊢
|
||||
· have ih := ih (h := h); simp [denote_eq] at ih ⊢
|
||||
have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
|
||||
have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih.symm
|
||||
simp at ih
|
||||
rw [ih]
|
||||
. by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
|
||||
. have ih := ih (h := h); simp [denote_eq] at ih ⊢
|
||||
· by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
|
||||
· have ih := ih (h := h); simp [denote_eq] at ih ⊢
|
||||
have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
|
||||
have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih
|
||||
simp at ih
|
||||
rw [ih]
|
||||
. have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
· have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
have ih := ih (h := h); simp [denote_eq] at ih ⊢
|
||||
rw [← Nat.add_assoc, ih, Nat.add_assoc]
|
||||
|
||||
|
|
@ -435,25 +435,25 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
|
|||
split <;> simp at h <;> try assumption
|
||||
rename_i k₁ v₁ m₁ k₂ v₂ m₂
|
||||
by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
|
||||
. apply ih; simp [denote_le] at h |-; assumption
|
||||
. by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
|
||||
. apply ih; simp [denote_le] at h |-; assumption
|
||||
. have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
· apply ih; simp [denote_le] at h |-; assumption
|
||||
· by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
|
||||
· apply ih; simp [denote_le] at h |-; assumption
|
||||
· have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
|
||||
. apply ih
|
||||
· apply ih
|
||||
simp [denote_le] at h |-
|
||||
have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
|
||||
apply Nat.le_sub_of_add_le
|
||||
simp [h]
|
||||
. by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
|
||||
. apply ih
|
||||
· by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
|
||||
· apply ih
|
||||
simp [denote_le] at h |-
|
||||
have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
|
||||
apply Nat.sub_le_of_le_add
|
||||
simp [h]
|
||||
. have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
· have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
apply ih
|
||||
simp [denote_le] at h |-
|
||||
rw [← Nat.add_assoc, ← Nat.add_assoc] at h
|
||||
|
|
@ -469,25 +469,25 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
|
|||
split at h <;> simp <;> try assumption
|
||||
rename_i k₁ v₁ m₁ k₂ v₂ m₂
|
||||
by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
|
||||
. have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
|
||||
. by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
|
||||
. have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
|
||||
. have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
· have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
|
||||
· by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
|
||||
· have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
|
||||
· have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
|
||||
by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
|
||||
. have ih := ih (h := h); simp [denote_le] at ih ⊢
|
||||
· have ih := ih (h := h); simp [denote_le] at ih ⊢
|
||||
have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
|
||||
have := Nat.add_le_of_le_sub (Nat.le_trans haux (Nat.le_add_left ..)) ih
|
||||
simp at this
|
||||
exact this
|
||||
. by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
|
||||
. have ih := ih (h := h); simp [denote_le] at ih ⊢
|
||||
· by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
|
||||
· have ih := ih (h := h); simp [denote_le] at ih ⊢
|
||||
have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
|
||||
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
|
||||
have := Nat.le_add_of_sub_le ih
|
||||
simp at this
|
||||
exact this
|
||||
. have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
· have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
|
||||
have ih := ih (h := h); simp [denote_le] at ih ⊢
|
||||
have := Nat.add_le_add_right ih (k₁ * Var.denote ctx v₁)
|
||||
simp at this
|
||||
|
|
@ -560,8 +560,8 @@ theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denot
|
|||
cases c; rename_i eq lhs rhs
|
||||
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
|
||||
by_cases h : eq = true <;> simp [h]
|
||||
. simp [Poly.denote_eq, Expr.toPoly]
|
||||
. simp [Poly.denote_le, Expr.toPoly]
|
||||
· simp [Poly.denote_eq, Expr.toPoly]
|
||||
· simp [Poly.denote_le, Expr.toPoly]
|
||||
|
||||
attribute [local simp] ExprCnstr.denote_toPoly
|
||||
|
||||
|
|
@ -569,8 +569,8 @@ theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPo
|
|||
cases c; rename_i eq lhs rhs
|
||||
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]
|
||||
by_cases h : eq = true <;> simp [h]
|
||||
. rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
|
||||
. rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]
|
||||
· rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
|
||||
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]
|
||||
|
||||
attribute [local simp] ExprCnstr.denote_toNormPoly
|
||||
|
||||
|
|
@ -593,10 +593,10 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
|
|||
have : (1 == 1) = true := rfl
|
||||
by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
|
||||
<;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
|
||||
. exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
|
||||
. rw [h]
|
||||
. exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
|
||||
. apply Nat.mul_le_mul_left _ h
|
||||
· exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
|
||||
· rw [h]
|
||||
· exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
|
||||
· apply Nat.mul_le_mul_left _ h
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -607,10 +607,10 @@ theorem PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ :
|
|||
simp [denote] at h₁ h₂
|
||||
simp [PolyCnstr.combine, denote]
|
||||
by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] at h₁ h₂ |-
|
||||
. rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
|
||||
. rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
|
||||
. rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
|
||||
. rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; apply Nat.add_le_add h₁ h₂
|
||||
· rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
|
||||
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
|
||||
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
|
||||
· rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; apply Nat.add_le_add h₁ h₂
|
||||
|
||||
attribute [local simp] PolyCnstr.denote_combine
|
||||
|
||||
|
|
@ -624,26 +624,26 @@ theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = so
|
|||
theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p = true) : p.denote ctx = 0 := by
|
||||
simp [isZero] at h
|
||||
split at h
|
||||
. simp
|
||||
. contradiction
|
||||
· simp
|
||||
· contradiction
|
||||
|
||||
theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) : p.denote ctx > 0 := by
|
||||
match p with
|
||||
| [] => contradiction
|
||||
| (k, v) :: p =>
|
||||
by_cases he : v == fixedVar <;> simp [he, isNonZero] at h ⊢
|
||||
. simp [eq_of_beq he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
|
||||
. have ih := of_isNonZero ctx h
|
||||
· simp [eq_of_beq he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
|
||||
· have ih := of_isNonZero ctx h
|
||||
exact Nat.le_trans ih (Nat.le_add_right ..)
|
||||
|
||||
theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by
|
||||
cases c; rename_i eq lhs rhs
|
||||
simp [isUnsat]
|
||||
by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
|
||||
. intro
|
||||
· intro
|
||||
| Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
|
||||
| Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
|
||||
. intro ⟨h₁, h₂⟩
|
||||
· intro ⟨h₁, h₂⟩
|
||||
simp [Poly.of_isZero, h₂]
|
||||
have := Nat.not_le_of_gt (Poly.of_isNonZero ctx h₁)
|
||||
simp [this]
|
||||
|
|
@ -652,9 +652,9 @@ theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid
|
|||
cases c; rename_i eq lhs rhs
|
||||
simp [isValid]
|
||||
by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
|
||||
. intro ⟨h₁, h₂⟩
|
||||
· intro ⟨h₁, h₂⟩
|
||||
simp [Poly.of_isZero, h₁, h₂]
|
||||
. intro h
|
||||
· intro h
|
||||
simp [Poly.of_isZero, h]
|
||||
have := Nat.zero_le (Poly.denote ctx rhs)
|
||||
simp [this]
|
||||
|
|
@ -696,8 +696,8 @@ theorem Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : c
|
|||
theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx := by
|
||||
simp [monomialToExpr]
|
||||
by_cases h : v == fixedVar <;> simp [h, Expr.denote]
|
||||
. simp [eq_of_beq h, Var.denote]
|
||||
. by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
|
||||
· simp [eq_of_beq h, Var.denote]
|
||||
· by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
|
||||
|
||||
attribute [local simp] denote_monomialToExpr
|
||||
|
||||
|
|
|
|||
|
|
@ -16,14 +16,14 @@ namespace Vector
|
|||
(v.snoc x).nth k = x := by
|
||||
cases k; rename_i k hk
|
||||
induction v generalizing k <;> subst h
|
||||
. simp only [nth]
|
||||
. simp_all[nth]
|
||||
· simp only [nth]
|
||||
· simp_all[nth]
|
||||
|
||||
theorem nth_snoc_eq_works (k: Fin (n+1))(v : Vector α n)
|
||||
(h: k.val = n):
|
||||
(v.snoc x).nth k = x := by
|
||||
cases k; rename_i k hk
|
||||
induction v generalizing k <;> subst h
|
||||
. simp only [nth]
|
||||
. simp[*,nth]
|
||||
· simp only [nth]
|
||||
· simp[*,nth]
|
||||
end Vector
|
||||
|
|
|
|||
|
|
@ -15,6 +15,6 @@ namespace Vector
|
|||
(h: v.mem y):
|
||||
f y ≤ v.foldr (λ x acc => max (f x) acc) init := by
|
||||
induction v <;> simp only[foldr,max]
|
||||
. admit
|
||||
. split <;> admit
|
||||
· admit
|
||||
· split <;> admit
|
||||
end Vector
|
||||
|
|
|
|||
|
|
@ -26,5 +26,5 @@ theorem pow_nonneg : ∀ m : Nat, 0 ^ m ≥ 0
|
|||
| 0 => by decide
|
||||
| m@(_+1) => by
|
||||
rw [zeropow]
|
||||
. decide
|
||||
. apply Nat.zero_lt_succ
|
||||
· decide
|
||||
· apply Nat.zero_lt_succ
|
||||
|
|
|
|||
|
|
@ -6,11 +6,11 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
|
|||
| n+2 => by
|
||||
rw [Nat.div_eq]
|
||||
split
|
||||
. rw [Nat.add_sub_self_right]
|
||||
· rw [Nat.add_sub_self_right]
|
||||
have := pack_loop_terminates n
|
||||
calc n/2 + 1 < Nat.succ n + 1 := Nat.add_le_add_right this 1
|
||||
_ < Nat.succ (n + 2) := Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.lt_succ_self _))
|
||||
. apply Nat.zero_lt_succ
|
||||
· apply Nat.zero_lt_succ
|
||||
|
||||
def pack (n: Nat) : List Nat :=
|
||||
let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
|
||||
|
|
|
|||
|
|
@ -19,8 +19,8 @@ theorem ex5 : g false true true = 3 := rfl
|
|||
theorem f_eq (h : a = true → b = true → False) : f a b = 3 := by
|
||||
simp [f]
|
||||
split
|
||||
. contradiction
|
||||
. rfl
|
||||
· contradiction
|
||||
· rfl
|
||||
|
||||
theorem ex6 : g x y z > 0 := by
|
||||
simp [g]
|
||||
|
|
|
|||
|
|
@ -37,9 +37,9 @@ def foo (xs : List Nat) : List Nat :=
|
|||
|
||||
theorem foo_main_eq (xs : List Nat) : foo xs = foo.match_1 (fun _ => List Nat) xs (fun _ => []) (fun x xs => let y := 2*x; foo.match_1 (fun _ => List Nat) xs (fun _ => []) (fun x xs => (y + x)::foo xs)) := by
|
||||
split
|
||||
. rfl
|
||||
. split
|
||||
. rfl
|
||||
. rfl
|
||||
· rfl
|
||||
· split
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
#check @foo_main_eq
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
|
||||
intro j low high
|
||||
by_cases h : i < a.size
|
||||
. unfold Array.isEqvAux at heqv
|
||||
· unfold Array.isEqvAux at heqv
|
||||
simp [h] at heqv
|
||||
have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
|
||||
by_cases heq : i = j
|
||||
. subst heq; exact heqv.1
|
||||
. exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
|
||||
. have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
|
||||
· subst heq; exact heqv.1
|
||||
· exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
|
||||
· have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
|
||||
subst heq
|
||||
exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
|
||||
termination_by _ => a.size - i
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by
|
||||
apply Iff.intro
|
||||
. intro h
|
||||
· intro h
|
||||
by_cases hp:p <;> by_cases hq:q
|
||||
. specialize h hp hq; contradiction
|
||||
. exact Or.inr hq
|
||||
. exact Or.inl hp
|
||||
. exact Or.inr hq
|
||||
. intro
|
||||
· specialize h hp hq; contradiction
|
||||
· exact Or.inr hq
|
||||
· exact Or.inl hp
|
||||
· exact Or.inr hq
|
||||
· intro
|
||||
| Or.inl hnp => intros; contradiction
|
||||
| Or.inr hnq => intros; contradiction
|
||||
|
|
|
|||
|
|
@ -9,19 +9,19 @@ example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → f x y z = 1 := by
|
|||
intros
|
||||
simp [f]
|
||||
split
|
||||
. contradiction
|
||||
. contradiction
|
||||
. contradiction
|
||||
. rfl
|
||||
· contradiction
|
||||
· contradiction
|
||||
· contradiction
|
||||
· rfl
|
||||
|
||||
example (x y z : Nat) : f x y z = y ∨ f x y z = 1 := by
|
||||
intros
|
||||
simp [f]
|
||||
split
|
||||
. exact Or.inl rfl
|
||||
. exact Or.inl rfl
|
||||
. exact Or.inl rfl
|
||||
. exact Or.inr rfl
|
||||
· exact Or.inl rfl
|
||||
· exact Or.inl rfl
|
||||
· exact Or.inl rfl
|
||||
· exact Or.inr rfl
|
||||
|
||||
example (x y z : Nat) : f x y z = y ∨ f x y z = 1 := by
|
||||
intros
|
||||
|
|
|
|||
|
|
@ -17,8 +17,8 @@ example (a b : Bool) (x y z : Nat) (xs : List Nat) (h1 : (if a then x else y) =
|
|||
|
||||
example (a : Bool) (h1 : (if a then x else y) = 1) : x + y > 0 := by
|
||||
split at h1
|
||||
. subst h1; rw [Nat.succ_add]; apply Nat.zero_lt_succ
|
||||
. subst h1; apply Nat.zero_lt_succ
|
||||
· subst h1; rw [Nat.succ_add]; apply Nat.zero_lt_succ
|
||||
· subst h1; apply Nat.zero_lt_succ
|
||||
|
||||
def f (x : Nat) : Nat :=
|
||||
match x with
|
||||
|
|
@ -29,9 +29,9 @@ def f (x : Nat) : Nat :=
|
|||
example (h1 : f x = 0) (h2 : x > 300) : False := by
|
||||
simp [f] at h1
|
||||
split at h1
|
||||
. contradiction
|
||||
. contradiction
|
||||
. contradiction
|
||||
· contradiction
|
||||
· contradiction
|
||||
· contradiction
|
||||
|
||||
example (h1 : f x = 0) (h2 : x > 300) : False := by
|
||||
simp [f] at h1
|
||||
|
|
|
|||
|
|
@ -61,9 +61,9 @@ example (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
|
|||
|
||||
example (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
|
||||
apply Eq.trans
|
||||
. sorry
|
||||
. sorry
|
||||
. sorry
|
||||
· sorry
|
||||
· sorry
|
||||
· sorry
|
||||
|
||||
example (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
|
||||
apply Eq.trans <;> sorry
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h
|
|||
unfold anyM.loop
|
||||
intro h
|
||||
split at h
|
||||
. simp [Bind.bind, pure] at h; split at h
|
||||
· simp [Bind.bind, pure] at h; split at h
|
||||
next he => subst a; apply sizeOf_get_lt
|
||||
next => have ih := aux (j+1) h; assumption
|
||||
. contradiction
|
||||
· contradiction
|
||||
apply aux 0 h
|
||||
termination_by aux j => as.size - j
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ theorem ex4 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by
|
|||
|
||||
theorem ex5 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by
|
||||
cases h1
|
||||
. skip -- Error here
|
||||
· skip -- Error here
|
||||
skip
|
||||
. skip -- Error here
|
||||
· skip -- Error here
|
||||
skip
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue