formal semantics example

test.lean

section TEST
 axiom x : Type
 axiom e : Type
 axiom _man_n_1 : x → Prop
 axiom _walk_v_1 : e → x → Prop

 -- a man is walking
 def h1a : Prop := ∃ e2 x3, _man_n_1 x3 ∧ _walk_v_1 e2 x3
 def h1b : Prop := ∃ x3, _man_n_1 x3 ∧ ∃ e2, _walk_v_1 e2 x3
 -- no man is walking
 def h3  : Prop := ∀ x3, _man_n_1 x3 → ¬ ∃ e2, _walk_v_1 e2 x3

 -- a man is not walking
 def h2a : Prop := ¬(∃ x3, _man_n_1 x3 ∧ ∃ e2, _walk_v_1 e2 x3)
 def h2b : Prop := ∃ x3, _man_n_1 x3 ∧ ¬ ∃ e2, _walk_v_1 e2 x3

 theorem test1 : (h1a ∧ h3) → False := by
  unfold h1a h3
  intro ⟨⟨n, h₁⟩, h₂⟩ 
  apply Exists.elim h₁ 
  intro b h₃
  apply (h₂ b)
  { exact h₃.left }
  { exists n; exact h₃.right }

 theorem test2 : (h1b ∧ h3) → False := by
  unfold h1b h3
  intro ⟨⟨n, h₁⟩ , h₂⟩ 
  apply (h₂ n)
  { exact h₁.left }
  { exact h₁.right }

 theorem test3 : (h1b ∧ h2a) → False := by
  unfold h1b h2a
  intro ⟨h₁, h₂⟩
  apply h₂ 
  exact h₁ 

 theorem test4 : (h1b ∧ h2b) → False := by
  unfold h1b h2b
  intro ⟨⟨n,h₁⟩ , ⟨ m, h₂⟩⟩  
  -- I don't know how to prove this one, 
  sorry

end TEST