lean proof

all-people.lean

section 
 constant u : Type

 -- constants from MRS
 constant named : u → String → Prop
 constant compound : u → u → u → Prop
 constant _electronics_n_1 : u → Prop
 constant _people_n_of : u → u → Prop
 constant _go_v_1 : u → u → Prop
 constant _to_p_dir : u → u → u → Prop
 constant _buy_v_1 : u → u → u → Prop

 -- constants from AMR
 constant store : u → Prop
 constant person : u → Prop
 constant electronics : u → Prop
 constant buy_01 : u → Prop
 constant go_02 : u → Prop
 constant ARG0 : u → u → Prop
 constant ARG0_of : u → u → Prop
 constant ARG1 : u → u → Prop
 constant ARG4 : u → u → Prop
 constant ALL : u → Prop
 constant mod : u → u → Prop
 constant name : u → Prop
 constant name1 : u → u → Prop
 constant op1 : u → String → Prop
 constant op2 : u → String → Prop

 -- mappings
 axiom s1 : ∀ e, buy_01 e ↔ ∃ x y,_buy_v_1 e x y
 axiom s2 : ∀ e, go_02 e ↔ ∃ x,_go_v_1 e x
 axiom s3 : electronics = _electronics_n_1  

 -- amr2logic 
 def a0 := ∃ b, (buy_01 b ∧ ∃ p, (person p ∧ ∃ g, (go_02 g ∧ ∃ s, (store s ∧ ∃ n, (name n ∧ op1 n "Apple" ∧ op2 n "Store" ∧ name1 s n) 
  ∧ ARG4 g s ) ∧ ARG0_of p g) ∧ ∃ a, (ALL a ∧ mod p a) ∧ ARG0 b p) ∧ ∃ e,(electronics e ∧ ARG1 b e))

 -- mrs2logic 
 def a1 := ∃ e2, ∃ i8, ∃ e9, ∃ e10, ∃ e16, ∃ x11, (∃ x17, named x17 "Apple" ∧ compound e16 x11 x17 ∧ named x11 "Store") 
  ∧ (∃ x24, _electronics_n_1 x24 ∧ (∀ x3, (_people_n_of x3 i8 ∧ _go_v_1 e9 x3 ∧ _to_p_dir e10 e9 x11) → _buy_v_1 e2 x3 x24))

 -- MRS+AMR manually simplified
 def a2 := ∃ e2 i8 e9 e10 x11 x24, named x11 "Apple Store" ∧ store x11 ∧ _electronics_n_1 x24 
  ∧ (∀ x3, (_people_n_of x3 i8 ∧ _go_v_1 e9 x3 ∧ _to_p_dir e10 e9 x11) → _buy_v_1 e2 x3 x24)

 -- prenex normal form
 def a21 := ∃ e2 i8 e9 e10 x11 x24, ∀ x3, named x11 "Apple Store" ∧ store x11 ∧ _electronics_n_1 x24 
   ∧ (_people_n_of x3 i8 ∧ _go_v_1 e9 x3 ∧ _to_p_dir e10 e9 x11 → _buy_v_1 e2 x3 x24)

 -- prenex conjunctive normal form
 def a22 := ∃ e2 i8 e9 e10 x11 x24, ∀ x3, 
   (named x11 "Apple Store" ∧ store x11 ∧ _electronics_n_1 x24 
   ∧ (¬_people_n_of x3 i8 ∨ ¬ _go_v_1 e9 x3 ∨ ¬_to_p_dir e10 e9 x11 ∨ _buy_v_1 e2 x3 x24)) 

 theorem t1 : a2 ↔ a21 := by 
  unfold a2
  unfold a21
  apply Iff.intro
  case mp =>
   intro ⟨a, b, c, d, e, f, pf⟩
   exists a; exists b; exists c; exists d; exists e; exists f; intro g
   apply And.intro; exact And.left pf
   apply And.intro; exact And.left $ And.right pf; 
   apply And.intro; exact And.left $ And.right $ And.right pf;
   exact (And.right $ And.right $ And.right pf) g;
  case mpr =>
   intro ⟨a, b, c, d, e, f, pf⟩
   exists a; exists b; exists c; exists d; exists e; exists f;
   apply And.intro; exact And.left (pf a);
   apply And.intro; exact And.left $ And.right $ pf a;
   apply And.intro; exact And.left $ And.right $ And.right $ pf a; 
   intro g; exact And.right $ And.right $ And.right $ pf g;

      
 theorem t2 : a2 ↔ a22 := sorry

end