feat: try_prove

Logic/AutoProver/TaitStyle.lean

@@ -164,10 +164,6 @@ open Denotation
 
 variable {F : Q(Type u)} {ls : Q(LogicSymbol $F)} {os : Q(OneSided.{u, v} $F)} (G : List (Lit F))
 
-abbrev DEqFun {F : Q(Type*)} (ls : outParam (Q(LogicSymbol $F))) (f : Q($F → $F)) (p q : Lit F) :=
-  letI := Lit.denotation F ls
-  Denotation.DEqFun f p q
-
 def DEq {F : Q(Type*)} : Lit F → Lit F → MetaM Bool
   | Formula.atom e,  Formula.atom e'  => Lean.Meta.isDefEq e e'
   | Formula.natom e, Formula.natom e' => Lean.Meta.isDefEq e e'
@@ -193,7 +189,7 @@ def verum : DerivationQ ls os (⊤ :: G) := q(OneSided.verum _)
 
 def emOfEq (dm : Q(DeMorgan $F)) {p : Lit F} (G) : MetaM (DerivationQ ls os (p :: G)) :=
   letI := Lit.denotation F ls
-  do let some h ← Denotation.memList? (Lit.denotation F ls) (~p) G | throwError m! "failed to prove {~p} ∈ {G}"
+  do let some h ← Denotation.memList? (Lit.denotation F ls) (~p) G | throwError m! "failed to derive {~p} ∈ {G}"
      let e : Q(~$(toExpr F p) = $(toExpr F $ ~p)) := q($(Lit.negToExprEqToExprNeg F ls dm p))
      return q(OneSided.emOfEq $e $h)
 
@@ -209,9 +205,9 @@ def rAnd {p q : Lit F} (dp : DerivationQ ls os (G ++ [p])) (dq : DerivationQ ls
   let xq : Q(OneSided.Derivation ($(Denotation.toExprₗ (Lit.denotation F ls) G) ++ [$(toExpr F q)])) := dq
   q(OneSided.rAnd $xp $xq)
 
-def prove {F : Q(Type u)} (ls : Q(LogicSymbol $F)) (dm : Q(DeMorgan $F)) (os : Q(OneSided.{u, v} $F)) :
+def derive {F : Q(Type u)} (ls : Q(LogicSymbol $F)) (dm : Q(DeMorgan $F)) (os : Q(OneSided.{u, v} $F)) :
     ℕ → (G : List (Lit F)) → MetaM (DerivationQ ls os G)
-  | 0,     _      => throwError "failed!"
+  | 0,     G      => throwError f!"failed! {G}"
   | _,     []     => throwError "empty goal"
   | s + 1, p :: G => do
     -- proof search
@@ -221,24 +217,108 @@ def prove {F : Q(Type u)} (ls : Q(LogicSymbol $F)) (dm : Q(DeMorgan $F)) (os : Q
     match p with
     | ⊤               => pure $ verum G
     | ⊥               => do
-      let d ← prove ls dm os s G
+      let d ← derive ls dm os s G
       return tail G d
     | p ⋎ q           => do
-      let d ← prove ls dm os s (G ++ [p, q])
+      let d ← derive ls dm os s (G ++ [p, q])
       return rOr G d
     | p ⋏ q           => do
-      let dp ← prove ls dm os s (G ++ [p])
-      let dq ← prove ls dm os s (G ++ [q])
+      let dp ← derive ls dm os s (G ++ [p])
+      let dq ← derive ls dm os s (G ++ [q])
       return rAnd G dp dq
     | Formula.atom a  => do
-      let d ← prove ls dm os s (G ++ [Formula.atom a])
+      let d ← derive ls dm os s (G ++ [Formula.atom a])
       return rotate G d
     | Formula.natom a => do
-      let d ← prove ls dm os s (G ++ [Formula.natom a])
+      let d ← derive ls dm os s (G ++ [Formula.natom a])
       return rotate G d
 
 end DerivationQ
 
+open Lit
+
+def prove {F : Q(Type u)}
+    (ls : Q(LogicSymbol $F)) (dm : Q(DeMorgan $F))
+    (sys : Q(System $F)) (_ : Q(LawfulOneSided.{u, v} $F))
+    (s : ℕ) (T : Q(Set $F)) (p : Q($F)) : MetaM Q($T ⊢ $p) :=
+  letI := Litform.Meta.denotation F ls; do
+  let lf : Litform.Meta.Lit F ← Denotation.denote F p
+  let l := ofLitform F lf
+  let p' := Denotation.toExpr F (toLitform F l)
+  let eq : Q($p = $p') := (toLitformOfLitform F ls dm lf).expr
+  let d' : Q(⊢ᴸ [$p']) ← DerivationQ.derive ls dm q(LawfulOneSided.toOneSided) s [l]
+  let b : Q($T ⊢ $p) := q(LawfulOneSided.toProof (Eq.symm $eq ▸ $d') $T)
+  return b
+
+elab "tryProve" n:(num)? : tactic => do
+  let s : ℕ :=
+    match n with
+    | some n => n.getNat
+    | none   => 16
+  let goalType ← Elab.Tactic.getMainTarget
+  let some ⟨.succ u, ty⟩ ← checkSortQ' goalType | throwError "error: not a type"
+  let ~q(@HasTurnstile.turnstile.{u} $F _ $ss $T $p) := ty | throwError "error: not a type 2"
+  let .some instLS ← trySynthInstanceQ (q(LogicSymbol.{u} $F) : Q(Type u))
+    | throwError m! "error: failed to find instance LogicSymbol {F}"
+  let .some instDM ← trySynthInstanceQ q(DeMorgan $F)
+    | throwError m! "error: failed to find instance DeMorgan {F}"
+  let .some instSys ← trySynthInstanceQ q(System $F)
+    | throwError m! "error: failed to find instance System {F}"
+  let .some instLOS ← trySynthInstanceQ q(LawfulOneSided.{u, u} $F)
+    | throwError m! "error: failed to find instance LawfulOneSided {F}"
+  let b ← prove instLS instDM instSys instLOS s T p
+  Lean.Elab.Tactic.closeMainGoal b
+
+def prove! {F : Q(Type u)}
+    (ls : Q(LogicSymbol $F)) (dm : Q(DeMorgan $F))
+    (sys : Q(System $F)) (_ : Q(LawfulOneSided.{u, v} $F))
+    (s : ℕ) (T : Q(Set $F)) (p : Q($F)) : MetaM Q($T ⊢! $p) :=
+  letI := Litform.Meta.denotation F ls; do
+  let lf : Litform.Meta.Lit F ← Denotation.denote F p
+  let l := ofLitform F lf
+  let p' := Denotation.toExpr F (toLitform F l)
+  let eq : Q($p = $p') := (toLitformOfLitform F ls dm lf).expr
+  let d' : Q(⊢ᴸ [$p']) ← DerivationQ.derive ls dm q(LawfulOneSided.toOneSided) s [l]
+  let b : Q($T ⊢! $p) := q(⟨LawfulOneSided.toProof (Eq.symm $eq ▸ $d') $T⟩)
+  return b
+
+#check @System.Provable
+
+elab "try_prove" n:(num)? : tactic => do
+  let s : ℕ :=
+    match n with
+    | some n => n.getNat
+    | none   => 16
+  let goalType ← Elab.Tactic.getMainTarget
+  let ty ← inferPropQ goalType
+  let ~q(@System.Provable $F $j $jj $T $p) := ty | throwError "error: not a type 2"
+  let .some instLS ← trySynthInstanceQ (q(LogicSymbol $F) : Q(Type u_2))
+    | throwError m! "error: failed to find instance LogicSymbol {F}"
+  let .some instDM ← trySynthInstanceQ q(DeMorgan $F)
+    | throwError m! "error: failed to find instance DeMorgan {F}"
+  let .some instSys ← trySynthInstanceQ q(System $F)
+    | throwError m! "error: failed to find instance System {F}"
+  let .some instLOS ← trySynthInstanceQ q(LawfulOneSided.{u_2,u_2} $F)
+    | throwError m! "error: failed to find instance LawfulOneSided {F}"
+  let b ← prove! instLS instDM instSys instLOS s T p
+  Lean.Elab.Tactic.closeMainGoal b
+
+section test
+
+variable (T : Theory ℕ) (p : Formula ℕ)
+
+example : T ⊢ p ⟶ p := by tryProve
+
+example : T ⊢ p ⟶ p ⋎ q := by tryProve
+
+example : T ⊢ q ⋎ p ⟷ p ⋎ q := by tryProve 5
+
+example : T ⊢! q ⋎ p ⋎ r ⟷ r ⋎ p ⋎ q := by try_prove
+
+example : T ⊢! ((p ⟶ q) ⟶ p) ⟶ p := by try_prove
+
+end test
+
 end TaitStyle
 
 end LO

Logic/Logic/System.lean

@@ -186,7 +186,7 @@ namespace LawfulOneSided
 
 variable {F : Type*} [LogicSymbol F] [System F] [LawfulOneSided F]
 
-lemma toProof {p : F} (b : ⊢ᴸ [p]) (T : Set F) : T ⊢ p :=
+def toProof {p : F} (b : ⊢ᴸ [p]) (T : Set F) : T ⊢ p :=
   System.weakening (toProofEmpty b) (Set.empty_subset T)
 
 end LawfulOneSided

Logic/Propositional/Basic.lean

@@ -0,0 +1,3 @@
+import Logic.Propositional.Basic.Formula
+import Logic.Propositional.Basic.Semantics
+import Logic.Propositional.Basic.Calculus

Logic/Propositional/Basic/Calculus.lean

@@ -66,6 +66,13 @@ protected def cast (d : ⊢ᴾᶜ[P] Δ) (e : Δ = Γ) : ⊢ᴾᶜ[P] Γ := cast
 @[simp] lemma length_cast (d : ⊢ᴾᶜ[P] Δ) (e : Δ = Γ) : (d.cast e).length = d.length := by
   rcases e with rfl; simp[DerivationCR.cast]
 
+def cutWeakening {P Q : Formula α → Prop} (h : ∀ p, P p → Q p) : ∀ {Δ}, ⊢ᴾᶜ[P] Δ → ⊢ᴾᶜ[Q] Δ
+  | _, axL Δ a hpos hneg  => axL Δ a hpos hneg
+  | _, verum Δ h            => verum Δ h
+  | _, and Δ p q dp dq      => and Δ p q (dp.cutWeakening h) (dq.cutWeakening h)
+  | _, or Δ p q d           => or Δ p q (d.cutWeakening h)
+  | _, cut Δ₁ Δ₂ p hp d₁ d₂ => cut Δ₁ Δ₂ p (h p hp) (d₁.cutWeakening h) (d₂.cutWeakening h)
+
 def weakening : ∀ {Δ}, ⊢ᴾᶜ[P] Δ → ∀ {Γ : Sequent α}, Δ ⊆ Γ → ⊢ᴾᶜ[P] Γ
   | _, axL Δ a hrel hnrel, Γ,   h => axL Γ a (h hrel) (h hnrel)
   | _, verum Δ htop,         Γ, h => verum Γ (h htop)
@@ -135,6 +142,34 @@ instance Proof : System (Formula α) where
       hleftHand := Set.Subset.trans b.hleftHand (Set.image_subset _ h),
       derivation := b.derivation }
 
+def DerivationCR.toDerivationCRWA
+  {P : Formula α → Prop} {Δ : Sequent α} (b : ⊢ᴾᶜ[P] Δ) (T : Theory α) : T ⊢ᴾᶜ[P] Δ where
+  leftHand := ∅
+  hleftHand := by simp
+  derivation := b.cast (by simp)
+
+def DerivationCRWA.toDerivationCWA {T : Theory α} {Δ} (b : T ⊢ᴾᶜ[P] Δ) : T ⊢' Δ where
+  leftHand := b.leftHand
+  hleftHand := b.hleftHand
+  derivation := b.derivation.cutWeakening (by simp)
+
+def DerivationCWA.toDerivationCWA {T : Theory α} {p : Formula α} (b : T ⊢ p) : T ⊢' {p} := b
+
+def DerivationCRWA.toProof {T : Theory α} {p : Formula α} (b : T ⊢ᴾᶜ[P] {p}) : T ⊢ p :=
+  b.toDerivationCWA
+
+instance : OneSided (Formula α) where
+  Derivation := fun Δ : List (Formula α) => ⊢ᴾᵀ (Δ.toFinset : Sequent α)
+  verum := fun Δ => DerivationCR.verum _ (by simp)
+  and := fun dp dq => by simpa using DerivationCR.and _ _ _ (by simpa using dp) (by simpa using dq)
+  or := fun d => by simpa using DerivationCR.or _ _ _ (by simpa using d)
+  wk := fun d ss => DerivationCR.weakening d (List.toFinset_mono ss)
+  em := fun {p} d hp => DerivationCR.em (p := p) (by simp) (by simp[hp])
+
+instance : LawfulOneSided (Formula α) where
+  toProofEmpty := fun b =>
+    DerivationCRWA.toProof (DerivationCR.toDerivationCRWA b ∅)
+
 end Propositional
 
 end LO

Logic/Propositional/Basic/Formula.lean

@@ -85,6 +85,14 @@ by simp[Wedge.wedge]
 @[simp] lemma or_inj (p₁ q₁ p₂ q₂ : Formula α) : p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂ :=
 by simp[Vee.vee]
 
+instance : DeMorgan (Formula α) where
+  verum := rfl
+  falsum := rfl
+  and := by simp
+  or := by simp
+  imply := by simp[imp_eq]
+  neg := by simp
+
 def complexity : Formula α → ℕ
 | ⊤       => 0
 | ⊥       => 0

Logic/Vorspiel/Meta.lean

@@ -44,6 +44,8 @@ def inferSortQ' (e : Expr) : MetaM ((u : Level) × (α : Q(Sort $u)) × Q($α))
     | throwError "not a type{indentExpr α}"
   pure ⟨u, α, e⟩
 
+
+
 -- given an Expr e representing type α : Sort u, returns u and q(α)
 def checkSortQ' (e : Expr) : MetaM (Option ((u : Level) × Q(Sort $u))) := do
   if let ⟨.succ u, α, e⟩ ← inferSortQ' e then
@@ -52,6 +54,10 @@ def checkSortQ' (e : Expr) : MetaM (Option ((u : Level) × Q(Sort $u))) := do
     else return none
   else return none
 
+-- TODO: fix
+def inferPropQ (e : Expr) : MetaM Q(Prop) := do
+  return e
+
 def inferSortQOfUniverse' (e : Expr) (ty : Q(Sort $u)) : MetaM (Option Q($ty)) := do
   if let ⟨.succ _, α, e⟩ ← inferSortQ' e then
     if ← isDefEq α q($ty) then