Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
import Pretty.Defs.Factory
import Pretty.Tactic
/-!
Basic facts about cost factories.
-/
namespace Factory
def lt ( F : Factory α ) ( c₁ c₂ : α ) : Prop :=
F . le c₁ c₂ ∧ c₁ ≠ c₂
section FactoryImplicit
variable { F : Factory α }
lemma le_refl ( c : α ) : F . le c c := by
dwi { cases F . le_total c c }
lemma not_eq_of_not_le : ∀ {c₁ c₂ : α }, ¬ le F c₁ c₂ = true c₁ ≠ c₂ not_eq_of_not_le ( h : ¬ F . le c₁ c₂ ) : c₁ ≠ c₂ := by
intro h'
subst h'
contrapose h
simp only [ Bool.not_eq_true , Bool.not_eq_false ]
apply le_refl
lemma not_le_iff_lt : ¬ F . le c₁ c₂ ↔ F . lt c₂ c₁ := by
constructor
case mp =>
intro h
simp only [ lt , ne_eq : ∀ {α : Sort ?u.572} (a b : α ), (a ≠ b = ¬ a = b ]
dwi { cases F . le_total c₂ c₁ }
case inl h' =>
simp only [ h' , true_and ]
intro h
dwi { apply not_eq_of_not_le }
. symm
assumption
case mpr =>
intro h
simp [ lt ] at *
let ⟨ h₁ , h₂ ⟩ := h
contrapose h₂
simp only [ ne_eq : ∀ {α : Sort ?u.1069} (a b : α ), (a ≠ b = ¬ a = b , Bool.not_eq_false ] at h₂
have h' := F . le_antisymm h₁ h₂
simpa
lemma lt_trans : ∀ {α : Type } {F : Factory α c₁ c₂ c₃ : α }, lt F c₁ c₂ lt F c₂ c₃ lt F c₁ c₃ lt_trans ( h₁ : F . lt c₁ c₂ ) ( h₂ : F . lt c₂ c₃ ) : F . lt c₁ c₃ := by
simp only [ lt , ne_eq : ∀ {α : Sort ?u.1349} (a b : α ), (a ≠ b = ¬ a = b ] at *
let ⟨ h₁ , _⟩ := h₁
let ⟨ h₂ , _⟩ := h₂
constructor
case left => dwi { apply F . le_trans }
case right =>
intro h
subst h
dwi { have := F . le_antisymm h₁ h₂ }
lemma le_of_lt : ∀ {c c' : α }, lt F c c' le F c c' = true le_of_lt ( h₁ : F . lt c c' ) : F . le c c' := by
simp only [ lt , ne_eq : ∀ {α : Sort ?u.1807} (a b : α ), (a ≠ b = ¬ a = b ] at h₁
simp [ h₁ ]
lemma invalid_inequality ( h₁ : F . le c₁ c₂ ) ( h₂ : F . lt c₂ c₃ ) ( h₃ : F . le c₃ c₁ ) : False := by
simp [ lt ] at h₂
have h_trans := F . le_trans h₁ h₂ . left : ∀ {a b : Prop }, a ∧ b a
have h := F . le_antisymm h_trans h₃
subst h
have h := F . le_antisymm h₁ h₂ . left : ∀ {a b : Prop }, a ∧ b a
subst h
simp at h₂
end FactoryImplicit
end Factory