revert

Auto/Translation/Monomorphization.lean

@@ -30,7 +30,7 @@ register_option auto.mono.recordInstInst : Bool := {
 }
 
 register_option auto.mono.allowGeneralExprAbst : Bool := {
-  defValue := true
+  defValue := false
   descr := "Apart from `ConstInst`s, allow general expressions to be abstracted" ++
            " " ++ "as free variables"
 }
@@ -728,6 +728,8 @@ namespace FVarRep
       unknownExpr2Expr e
     else
       unknownExpr2FVar e
+
+  -- **TODO:** Only go into non-dependent arguments for the `.app` case
   /--
     Attempt to abstract parts of a given expression to free variables so
     that the resulting expression is in the higher-order fragment of Lean.

Test/Bugs.lean

@@ -11,7 +11,7 @@ set_option auto.tptp.zeport.path "/home/indprinciple/Programs/zipperposition/por
 set_option trace.auto.smt.printCommands true
 set_option trace.auto.smt.result true
 set_option auto.smt.solver.name "z3"
--- Standard Native Configs
+-- Emulate native solver
 set_option trace.auto.native.printFormulas true
 set_option auto.native.solver.func "Auto.Solver.Native.emulateNative"
 
@@ -24,5 +24,58 @@ set_option trace.auto.lamReif.printValuation true
 
 set_option trace.auto.mono true
 
-example (h1 : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0) (h2 : 3 > 0) : ∃ z : Fin 3, z.1 = 0 := by
+/--
+  h₁ : ∀ x : Nat, x > 0 → ∃ y : Fin x, @Fin.val x y = 0
+  h₂ : 3 > 0
+  ngoal : ¬ ∃ z : Fin 3, @Fin.val 3 z = 0
+
+  Abstracted: fun x => ∃ y : Fin x, @Fin.val x y
+-/
+example
+  (h₁ : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0)
+  (h₂ : 3 > 0) : ∃ z : Fin 3, z.1 = 0 := by
+  auto
+
+/--
+  h₁ : ∀ x : Nat, x > 0 → ∃ y : Fin x, @Fin.val x y = 0
+  h₂ : 3 > 0
+  ngoal : ¬ ∃ z : Fin (f 3), @Fin.val (f 3) z = 0
+
+  Abstracted: fun x => ∃ y : Fin x, @Fin.val x y
+-/
+example
+  (f : Nat → Nat)
+  (h₁ : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0)
+  (h₂ : ∀ x, f x > 0):
+  ∃ z : Fin (f 3), @Fin.val (f 3) z = 0 := by
+  generalize f 3 = u
+
+section Set
+
+  opaque Set : Type u → Type u
+
+  opaque mem_set : ∀ {α : Type u}, Set α → (α → Prop)
+
+  axiom setOf.{u} : ∀ (α : Type u), (α → Prop) → Set α
+
+  axiom iUnion.{u, v} : ∀ (α : Type u) (ι : Sort v), (ι → Set α) → Set α
+
+  axiom mem_iUion.{u, v} : ∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, mem_set (iUnion _ _ s) x ↔ ∃ i, mem_set (s i) x
+
+  example
+    (dvd : Nat → Nat → Prop)
+    (primeset : Set Nat) :
+    iUnion Nat Nat (fun p => iUnion Nat (mem_set primeset p) (fun h => setOf Nat (fun x => dvd p x))) =
+    setOf Nat (fun x => ∃ p, mem_set primeset p ∧ dvd p x) := by
+    auto
+
+end Set
+
+/--
+  ∃ (i : Nat) (i_1 : primeset i), dvd i x
+
+  Abstracted : fun i f => ∃ (i_1 : primeset i), f i
+-/
+example (x : Nat) (primeset : Nat → Prop) (dvd : Nat → Nat → Prop) :
+  ((∃ (i : _) (i_1 : primeset i), dvd i x) ↔ (∃ p, primeset p ∧ dvd p x)) := by
   auto