Lean4
/-- Insert a proposition and its proof into the context, as in `have : A := p`. This will eagerly
apply all level 1 rules on the spot, which are rules that don't split the goal and are validity
preserving: specifically, we drop `⊤` and `A → ⊤` hypotheses, close the goal if we find a `⊥`
hypothesis, split all conjunctions, and also simplify `⊥ → A` (drop), `⊤ → A` (simplify to `A`),
`A ∧ B → C` (curry to `A → B → C`) and `A ∨ B → C` (rewrite to `(A → C) ∧ (B → C)` and split). -/
partial def add : IProp → Proof → Context → Except (IProp → Proof) Context
| .true, _, Γ => pure Γ
| .false, p, _ => throw fun A => .exfalso A p
| .and' ak A B, p, Γ => do
let (A, B) := ak.sides A B
let Γ ← Γ.add A (p.andLeft ak)
Γ.add B (p.andRight ak)
| .imp .false _, _, Γ => pure Γ
| .imp .true A, p, Γ => Γ.add A (p.app .triv)
| .imp (.and' ak A B) C, p, Γ =>
let (A, B) := ak.sides A B
Γ.add (A.imp (B.imp C)) (p.curry ak)
| .imp (.or A B) C, p, Γ => do
let Γ ← Γ.add (A.imp C) p.orImpL
Γ.add (B.imp C) p.orImpR
| .imp _ .true, _, Γ => pure Γ
| A, p, Γ => pure (Γ.insert A p)
