Add support for explicitly Finite non-implications (#702)

As discussed in [1], I add support to the @[equational_result] attribute
to parse non-implication theorems with Finite typeclasses. I then add
support to `extract_implications` to specify `--finite-only` to limit
results to finite non-implications.

In addition, I also add some additional checking to @[equational_result]
as previously it would silently mis-parse theorems with the Finite
typeclass.

This was tested by generating `extract_implications` closure/unknowns
results before and after this change. When I included finite
non-implications (not in this change), the results correctly showed them
with `--finite-only`, while the results without `--finite-only` did not
change and match the results prior to this change.

[1]
https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Proposal.3A.20Add.20Finite.20typeclasses.20to.20non-implications/near/477933508

equational_theories/Closure.lean

@@ -170,7 +170,7 @@ def equationSet (inp : Array EntryVariant) : Std.HashSet String := Id.run do
     | .implication ⟨lhs, rhs⟩ =>
       eqs := eqs.insert lhs
       eqs := eqs.insert rhs
-    | .facts ⟨satisfied, refuted⟩ =>
+    | .facts ⟨satisfied, refuted, _⟩ =>
       for eq in satisfied ++ refuted do
         eqs := eqs.insert eq
     | .unconditional eq =>
@@ -192,7 +192,7 @@ def toEdges (inp : Array EntryVariant) : Array Edge := Id.run do
     match imp with
     | .implication ⟨lhs, rhs⟩ =>
       edges := edges.push (.implication ⟨lhs, rhs⟩)
-    | .facts ⟨satisfied, refuted⟩ =>
+    | .facts ⟨satisfied, refuted, _⟩ =>
       for f1 in satisfied do
         for f2 in refuted do
           nonimplies := nonimplies.modify eqs[f1]! (fun x ↦ x.set eqs[f2]!)
@@ -221,7 +221,7 @@ def closure_aux (inp : Array EntryVariant) (duals: Std.HashMap Nat Nat) (eqs : D
       graph := graph.modify (eqs[imp.rhs]! + n) (fun x => x.push (eqs[imp.lhs]! + n))
       revgraph := revgraph.modify (eqs[imp.lhs]!) (fun x => x.push eqs[imp.rhs]!)
       revgraph := revgraph.modify (eqs[imp.lhs]! + n) (fun x => x.push (eqs[imp.rhs]! + n))
-    | .facts ⟨satisfied, refuted⟩ =>
+    | .facts ⟨satisfied, refuted, _⟩ =>
       if satisfied.size * refuted.size < satisfied.size + refuted.size + 1 then
         for lhs in satisfied do
           for rhs in refuted do

equational_theories/EquationalResult.lean

@@ -61,11 +61,11 @@ def Entry.keepCore (e : Entry) : Option Entry :=
       if isCoreEquationName lhs && isCoreEquationName rhs
       then some e
       else none
-  | .facts { satisfied, refuted } =>
+  | .facts { satisfied, refuted, finite } =>
       let sat1 := satisfied.filterMap filterCoreEquationName
       let ref1 := refuted.filterMap filterCoreEquationName
       if sat1.isEmpty || ref1.isEmpty then none
-      else some <| {e with variant := .facts {satisfied := sat1, refuted := ref1}}
+      else some <| {e with variant := .facts {satisfied := sat1, refuted := ref1, finite := finite}}
   | .unconditional eq => if isCoreEquationName eq then some e else none
 
 namespace Result
@@ -149,7 +149,7 @@ elab_rules : command
   for ⟨name, _filename, res, _⟩ in rs do
     match res with
     | .implication ⟨lhs, rhs⟩ => println! "{name}: {lhs} → {rhs}"
-    | .facts ⟨satisfied, refuted⟩ => println! "{name}: {satisfied} // {refuted}"
+    | .facts ⟨satisfied, refuted, _⟩ => println! "{name}: {satisfied} // {refuted}"
     | .unconditional rhs => println! "{name}: {rhs} holds unconditionally"
 
 end Result

equational_theories/ParseImplications.lean

@@ -27,6 +27,7 @@ the four antiimplications `¬ 1→4`, `¬ 1→5`, `¬ 2→4`, `¬ 2→5`.
 structure Facts where
   satisfied : Array String
   refuted : Array String
+  finite : Bool
 deriving Lean.ToJson, Lean.FromJson, Inhabited
 
 /--
@@ -37,7 +38,11 @@ def getEquationName (app : Expr) : Option String := do
   | (.app (.app (.const name _) _) _) =>
     -- Copy the string to allow it to safely escape from `Lean.withImportModules`.
     -- Otherwise, segfaults are possible.
-    some ("" ++ name.toString)
+    let copy := name.toString
+    if copy.startsWith "Equation" then
+      some ("" ++ copy)
+    else
+      none
   | _ => none
 
 def getEquationLeanName (app : Expr) : Option Lean.Name := do
@@ -157,17 +162,27 @@ partial def parseFacts (thm_ty : Expr) : MetaM (Option Facts) := do
         Meta.lambdaTelescope body1 fun fvars1 ty1 => do
           let #[magma] := fvars1 | return none
           let (.app (.const `Magma _) _) := ← Meta.inferType magma | return none
-          let some facts := go #[ty1] #[] #[] | return none
-          if facts.satisfied.isEmpty && facts.refuted.isEmpty then return none
-          return .some facts
+          match_expr ty1 with
+          | Exists b2 body2 =>
+            let (.app (.const `Finite _) _) := b2 | return none
+            Meta.lambdaTelescope body2 fun _ ty2 => do
+              return ← parseList ty2 true
+          | _ => return ← parseList ty1 false
       | _ => return none
   | _ => return none
 where
+  parseList (ty : Expr) (finite : Bool) : MetaM (Option Facts) := do
+    let some facts := go #[ty] #[] #[] | return none
+    if facts.satisfied.isEmpty && facts.refuted.isEmpty then return none
+    if facts.satisfied.isEmpty || facts.refuted.isEmpty then
+      Lean.logWarning "Warning: Facts statement has empty satisfied or refuted list"
+    return .some { facts with finite := finite }
+
   -- NB: This is written as a tail-recursive function, else some large facts statements
   -- cause this to blow the stack
   go (todo : Array Expr) (satisfied refuted : Array String) : Option Facts := do
     if todo.isEmpty then
-      return ⟨satisfied, refuted⟩
+      return ⟨satisfied, refuted, false⟩
     else
       let e := todo.back
       let todo := todo.pop

scripts/extract_implications.lean

@@ -26,12 +26,16 @@ def withExtractedResults (imp : Cli.Parsed) (action : Array Entry → DualityRel
 def generateUnknowns (inp : Cli.Parsed) : IO UInt32 := do
   let only_e_c := inp.hasFlag "equivalence_creators"
   let duality := inp.hasFlag "duality"
+  let finite_only := inp.hasFlag "finite-only"
   let include_extra := inp.hasFlag "extra"
   if duality && include_extra then
     throw $ IO.userError "Cannot use both --duality and --extra"
   withExtractedResults inp fun rs dualityRelation => do
     let rs := if include_extra then rs else rs.filterMap Entry.keepCore
     let rs := if inp.hasFlag "proven" then rs.filter (·.proven) else rs
+    let rs := if !finite_only then rs else rs.filter (fun r =>
+      r.variant matches .implication .. || r.variant matches .facts { finite := true, .. }
+    )
     let rs := rs.map (·.variant)
     let (components, outcomes) ← Closure.outcomes_mod_equiv rs dualityRelation.dualEquations
     let sortedComponents := components.in_order.qsort (fun a b => Closure.ltEquationNames a[0]! b[0]!)
@@ -79,6 +83,7 @@ def unknowns : Cmd := `[Cli|
     equivalence_creators; "Output only implications whose converse is known to be true"
     extra; "Include extra equations that are not in the core set"
     duality; "Only include one implication of each dual pair"
+    "finite-only"; "Only report finite results"
 
   ARGS:
     ...files : Array ModuleName; "The files to extract the implications from"
@@ -93,7 +98,7 @@ structure Output where
 structure OutputOutcomes where
   equations : Array String
   outcomes : Array (Array Closure.Outcome)
-  deriving Lean.ToJson
+deriving Lean.ToJson
 
 --- Output of the extract_implications raw subcommand.
 structure OutputRaw where
@@ -136,9 +141,13 @@ def outcomes : Cmd := `[Cli|
 def generateOutput (inp : Cli.Parsed) : IO UInt32 := do
   let include_conj := inp.hasFlag "conjecture"
   let include_impl := inp.hasFlag "closure"
+  let finite_only := inp.hasFlag "finite-only"
   let only_implications := inp.hasFlag "only-implications"
   withExtractedResults inp fun rs dualityRelation => do
     let rs := if include_conj then rs else rs.filter (·.proven)
+    let rs := if !finite_only then rs else rs.filter (fun r =>
+      r.variant matches .implication .. || r.variant matches .facts { finite := true, .. }
+    )
     let rs := if only_implications then rs.filter (·.variant matches .implication ..) else rs
     let rs := rs.map (·.variant)
     let rs ← if include_impl then Closure.closure rs dualityRelation.dualEquations else pure (Closure.toEdges rs)
@@ -185,6 +194,7 @@ def extract_implications : Cmd := `[Cli|
     closure; "Compute the transitive closure"
     json; "Output the data as JSON"
     "only-implications"; "Only consider implications"
+    "finite-only"; "Only report finite results"
 
   ARGS:
     ...files : Array ModuleName; "The files to extract the implications from"