Proof reconstruction for currently implemented datatype exhaustivenes…

…s fragment (still no polymorphism support)

Duper/Rules/DatatypeExhaustiveness.lean

@@ -6,6 +6,13 @@ open ProverM RuleM Lean Meta
 
 initialize Lean.registerTraceClass `duper.rule.datatypeExhaustiveness
 
+/-- Given an expression `∀ x1 : t1, x2 : t2, ... xn : tn, b`, returns `[t1, t2, ..., tn]`. If the given expression is not
+    a forall expression, then `getForallArgumentTypes` just returns the empty list -/
+partial def getForallArgumentTypes (e : Expr) : List Expr :=
+  match e.consumeMData with
+  | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
+  | _ => []
+
 def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
   Meta.forallTelescope c.toForallExpr fun xs body => do
     let emptyTypeFVar := xs[xs.size - 1]!
@@ -15,12 +22,72 @@ def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List Pro
     let motive := .lam `_ emptyType (mkConst ``False) .default -- motive is `fun _ : emptyType => False`
     mkLambdaFVars xs $ ← mkAppM' (mkConst (.str emptyTypeName "casesOn") (0 :: lvls)) #[motive, emptyTypeFVar]
 
-/-- Given an expression `∀ x1 : t1, x2 : t2, ... xn : tn, b`, returns `[t1, t2, ..., tn]`. If the given expression is not
-    a forall expression, then `getForallArgumentTypes` just returns the empty list -/
-partial def getForallArgumentTypes (e : Expr) : List Expr :=
-  match e.consumeMData with
-  | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
-  | _ => []
+def mkDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
+  Meta.forallTelescope c.toForallExpr fun xs body => do
+    let cLits := c.lits.map (fun l => l.map (fun e => e.instantiateRev xs))
+    let idtFVar := xs[xs.size - 1]!
+    let idt ← inferType idtFVar
+    let some (idtIndVal, lvls) ← matchConstInduct idt.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival, lvls)))
+      | throwError "mkDatatypeExhaustivenessProof :: {idt} is not an inductive datatype"
+    let idtArgs := idt.getAppArgs.map some -- Mapping `some` to each element so it can be passed into `mkAppOptM'`
+    let constructors ← idtIndVal.ctors.mapM getConstInfoCtor
+    let motive ← mkLambdaFVars #[idtFVar] body
+    let mut casesOnArgs := #[] -- Each of these is an expression of type `∀ ctorFields, motive (ctor ctorFields)`
+    for ctor in constructors do
+      let orIdx := idtIndVal.numCtors - ctor.cidx - 1
+      let ctorBeforeFields ← mkAppOptM' (mkConst ctor.name lvls) idtArgs
+      let ctorType ← inferType ctorBeforeFields
+      let ctorArgTypes := getForallArgumentTypes ctorType
+      let curCasesOnArg ←
+        if ctorArgTypes.isEmpty then
+          let rflProof ← mkAppM ``Eq.refl #[ctorBeforeFields]
+          let idtFVarSubst := {map := AssocList.cons idtFVar.fvarId! ctorBeforeFields AssocList.nil}
+          let cLits := cLits.map (fun l => l.map (fun e => e.applyFVarSubst idtFVarSubst))
+          orIntro (cLits.map Lit.toExpr) orIdx rflProof
+        else
+          withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs => do
+            let fullyAppliedCtor ← mkAppM' ctorBeforeFields ctorArgs
+            let existsProof ←
+              withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs' => do
+                /-  Suppose ctorArgs = #[ctorArg0, ctorArg1] and ctorArgs' = #[ctorArg0', ctorArg1']
+                    Then we need to build:
+                    - @Exists.intro _ p1 ctorArg1 $ @Exists.intro _ p0 ctorArg0 $ Eq.refl (ctor ctorArg0 ctorArg1)
+                    Where:
+                    - p0 = `fun x => ctor ctorArg0 ctorArg1 = ctor x ctorArg1` (made via mkLambdaFVars #[ctorArg0']...)
+                    - p1 = `fun y => ∃ x : ctorArg1Type, ctor ctorArg0 ctorArg1 = ctor x y` -/
+                let mut rhsCtorArgs := ctorArgs
+                rhsCtorArgs := rhsCtorArgs.set! 0 ctorArgs'[0]!
+                let baseEquality ← mkAppM ``Eq #[fullyAppliedCtor, ← mkAppM' ctorBeforeFields rhsCtorArgs]
+                let existsIntroArg ← mkLambdaFVars #[ctorArgs'[0]!] baseEquality
+                let baseRflProof ← mkAppM ``Eq.refl #[fullyAppliedCtor]
+                let mut existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArgs[0]!, some baseRflProof]
+                let mut ctorArgNum := 0
+                trace[duper.rule.datatypeExhaustiveness] "Before entering loop, existsProof: {existsProof} (type: {← inferType existsProof})"
+                for (ctorArg, ctorArg') in ctorArgs.zip ctorArgs' do
+                  if ctorArgNum = 0 then
+                    ctorArgNum := 1
+                    continue
+                  rhsCtorArgs := rhsCtorArgs.set! ctorArgNum ctorArgs'[ctorArgNum]!
+                  let innerExistsProp ← do
+                    let mut innerExistsProp ← mkAppM ``Eq #[fullyAppliedCtor, ← mkAppM' ctorBeforeFields rhsCtorArgs]
+                    for i in [0:ctorArgNum] do
+                      innerExistsProp ← mkLambdaFVars #[ctorArgs'[i]!] innerExistsProp
+                      innerExistsProp ← mkAppM ``Exists #[innerExistsProp]
+                    pure innerExistsProp
+                  let existsIntroArg ← mkLambdaFVars #[ctorArg'] innerExistsProp
+                  existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArg, some existsProof]
+                  ctorArgNum := ctorArgNum + 1
+                  trace[duper.rule.datatypeExhaustiveness] "End of iteration {ctorArgNum} of loop"
+                  trace[duper.rule.datatypeExhaustiveness] "existsProof: {existsProof} (type: {← inferType existsProof})"
+                pure existsProof
+            let existsProof ← mkAppM ``eq_true #[existsProof]
+            let idtFVarSubst := {map := AssocList.cons idtFVar.fvarId! fullyAppliedCtor AssocList.nil}
+            let cLits := cLits.map (fun l => l.map (fun e => e.applyFVarSubst idtFVarSubst))
+            let orProof ← orIntro (cLits.map Lit.toExpr) orIdx existsProof
+            mkLambdaFVars ctorArgs orProof
+      trace[duper.rule.datatypeExhaustiveness] "casesOnArg for {ctor.name}: {curCasesOnArg} (type: {← inferType curCasesOnArg})"
+      casesOnArgs := casesOnArgs.push $ some curCasesOnArg
+    mkLambdaFVars xs $ ← mkAppOptM' (mkConst (.str idtIndVal.name "casesOn") (0 :: lvls)) (idtArgs ++ #[some motive, some idtFVar] ++ casesOnArgs)
 
 /-- Creates the expression `(∃ fields, e = ctor.{lvls} params fields) = True` where `params` are the inductive datatype's parameters
     and `fields` are arguments that need to be passed into `ctor` for the resulting expression to have the correct inductive type -/
@@ -66,8 +133,7 @@ def generateDatatypeExhaustivenessFact (idt : Expr) : ProverM Unit := do
       let cExp ← mkForallFVars #[idtFVar] cBody
       let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
       let c := Clause.fromForallExpr paramNames cExp
-      let mkProof := fun _ _ _ _ => Lean.Meta.mkSorry cExp (synthetic := true)
-      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkProof} maxGoalDistance 0 #[]
+      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
 
 /-- For each inductive datatype in `inductiveDataTypes`, generates an exhaustiveness lemma
     (e.g. `∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'`) and adds it to the passive set -/

Duper/Tests/test_regression.lean

@@ -748,3 +748,27 @@ example : ¬∃ x : Empty, True := by
 set_option duper.collectDatatypes true in
 example : ¬∃ x : (myEmpty Prop Type), True := by
   duper
+
+set_option duper.collectDatatypes true in
+example : ∀ x : myType, x = const1 ∨ x = const2 := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ∀ x : Type 1, ∀ y : Type 2, ¬∃ z : (myEmpty y x), True := by
+  duper
+
+set_option duper.collectDatatypes true in
+example : ∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l' := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ¬(∃ n : Nat, n ≠ 0 ∧ ∀ m : Nat, n ≠ m + 1) := by
+  duper [Nat.succ_eq_add_one] {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ∀ α : Type 2, ∀ x : myType2 α, ∃ t : α, x = const3 t ∨ ∃ t : α, x = const4 t := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example (t1 : Type 1) (t2 : Type 2) (x : myType4 t1 t2) :
+  ∃ y : t1, ∃ z : t2, x = const7 y z := by duper {portfolioInstance := 7}