Merge pull request #19 from leanprover-community/dev

Dev

Duper/Order.lean

@@ -85,7 +85,7 @@ def getHead (t : Expr) := match t with
 | Expr.forallE .. => mkConst ``FORALL
 | Expr.app (Expr.app (Expr.const ``Exists _) _) _  => mkConst ``EXISTS
 | Expr.mdata _ t => getHead t
-| _ => t.getAppFn
+| _ => t.getAppFn'
 
 def getArgs (t : Expr) := match t with
 | Expr.lam _ ty b _ => [ty, b]
@@ -396,7 +396,7 @@ def precCompare (f g : Expr) (symbolPrecMap : SymbolPrecMap) : MetaM Comparison
 /-- Overapproximation of being fluid -/
 def isFluid (t : Expr) :=
   let t := t.consumeMData
-  (t.isApp && t.getAppFn.isMVar') || (t.isLambda && t.hasMVar)
+  (t.isApp && t.getAppFn'.isMVar') || (t.isLambda && t.hasMVar)
 
 mutual
 

Duper/Rules/BoolSimp.lean

@@ -223,19 +223,10 @@ partial def mkRule26Theorem (e : Expr) (counter : Nat) (i : Nat) (j : Nat) : Met
     let iIdx := (counter - 1) - i
     orIntro goals j (Expr.bvar iIdx)
 
-/-- Assuming e has the form e1 ∧ e2 ∧ ... ∧ en, returns an array #[e1, e2, ... en].
-    Note: If e has the form (e1a ∧ e1b) ∧ e2 ∧ ... ∧ en, then the conjunction (e1a ∧ e1b) will
-    be considered e1 (and the conjunction e1 will not be broken down further). This decision is made
-    to reflect the form of the conjunction assumed by ProofReconstruction.lean's `andGet` -/
-partial def getConjunctiveHypotheses (e : Expr) (hyps : Array Expr) : Array Expr :=
-  match e.consumeMData with
-  | Expr.app (Expr.app (Expr.const ``And _) e1) e2 => getConjunctiveHypotheses e2 (hyps.push e1)
-  | _ => hyps.push e
-
 partial def mkRule27Theorem (e : Expr) (i : Nat) (j : Nat) : MetaM Expr := do
   match e.consumeMData with
   | Expr.forallE _ t b _ =>
-    let hyps := (getConjunctiveHypotheses t #[]).toList
+    let hyps := getConjunctiveHypotheses t
     let goals := getDisjunctiveGoals b #[]
     let iHypProof ← andGet hyps i (Expr.bvar 0)
     let innerBody ← orIntro goals j iHypProof
@@ -547,7 +538,7 @@ partial def applyRule27 (e : Expr) : RuleM (Option (Nat × Nat)) := do
   | e@(Expr.forallE ..) => Meta.forallBoundedTelescope e (some 1) fun xs b => do
     if !(← inferType b).isProp then return none -- Prevents applying rule27 to expressions like Nat → Nat
     let t ← inferType xs[0]!
-    let hyps := getConjunctiveHypotheses t #[]
+    let hyps := getConjunctiveHypothesesHelper t
     let goals := getDisjunctiveGoals b #[]
     let mut goalIdx := 0
     for goal in goals do

Duper/Rules/DatatypeAcyclicity.lean

@@ -0,0 +1,95 @@
+import Duper.Simp
+import Duper.Util.ProofReconstruction
+
+namespace Duper
+open Std
+open RuleM
+open SimpResult
+open Lean
+open Meta
+open LitSide
+
+initialize Lean.registerTraceClass `duper.rule.datatypeAcyclicity
+
+/-- Produces a list of (possibly duplicate) constructor subterms for `e` -/
+partial def collectConstructorSubterms (e : Expr) : MetaM (Array Expr) := do
+  let isConstructor ← matchConstCtor e.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
+  if isConstructor then
+    let constructorSubterms ← e.getAppArgs.mapM (fun arg => collectConstructorSubterms arg)
+    return constructorSubterms.flatten.push e
+  else
+    return #[e]
+
+/-- Returns `none` if `lit` does not compare constructor subterms, and returns `some litside` if `lit.litside`
+    is a subterm of the constructor it is being compared to. Note that `lit.litside` may not itself be a constructor
+    (e.g. `xs` is a constructor subterm of `x :: xs`) -/
+def litComparesConstructorSubterms (lit : Lit) : MetaM (Option LitSide) := do
+  let litTyIsInductive ← matchConstInduct lit.ty.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
+  if litTyIsInductive then
+    trace[duper.rule.datatypeAcyclicity] "lit.ty {lit.ty} is an inductive datatype"
+    -- If `e1` is a constructor subterm of `e2`, then `e1.weight ≤ e2.weight`
+    if lit.lhs.weight < lit.rhs.weight then
+      let rhsConstructorSubterms ← collectConstructorSubterms lit.rhs
+      if rhsConstructorSubterms.contains lit.lhs then return some lhs
+      else return none
+    else if lit.rhs.weight < lit.lhs.weight then
+      let lhsConstructorSubterms ← collectConstructorSubterms lit.lhs
+      if lhsConstructorSubterms.contains lit.rhs then return some rhs
+      else return none
+    else
+      if lit.lhs == lit.rhs then return some lhs
+      else return none
+  else -- `lit.ty` is not an inductive datatype so `lit` cannot be comparing constructor subterms
+    trace[duper.rule.datatypeAcyclicity] "lit.ty {lit.ty} is not an inductive datatype"
+    return none
+
+def mkDatatypeAcyclicityProof (removedLitNum : Nat) (litSide : LitSide) (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 (parentsLits, appliedPremises, transferExprs) ← instantiatePremises parents premises xs transferExprs
+    let parentLits := parentsLits[0]!
+    let appliedPremise := appliedPremises[0]!
+    let mut proofCases : Array Expr := Array.mkEmpty parentLits.size
+    for i in [:parentLits.size] do
+      let lit := parentLits[i]!
+      if i == removedLitNum then -- `lit` is the equality asserting an acyclic constructor
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          let sizeOfInst ← mkAppOptM ``inferInstanceAs #[← mkAppOptM ``SizeOf #[lit.ty], none]
+          let litTyMVar ← mkFreshExprMVar lit.ty
+          let abstrLam ← mkLambdaFVars #[litTyMVar] $ ← mkAppOptM ``sizeOf #[some lit.ty, some sizeOfInst, some litTyMVar]
+          let sizeOfEq ← mkAppM ``congrArg #[abstrLam, h] -- Has the type `sizeOf lit.lhs = sizeOf lit.rhs`
+          let sizeOfEqFalseMVar ← mkFreshExprMVar $ ← mkAppM ``Not #[← inferType sizeOfEq] -- Has the type `¬(sizeOf lit.lhs = sizeOf lit.rhs)`
+          let sizeOfEqFalseMVarId := sizeOfEqFalseMVar.mvarId!
+          -- **TODO**: Figure out how to assign `sizeOfEqFalseMVar` an actual term (ideally generated by `simp_arith`)
+          -- The below lines attempts to use the omega procedure to generate a term for `sizeOfEqFalseMVar`, but it doesn't work
+          Elab.Tactic.Omega.omega [] sizeOfEqFalseMVarId -- Use the `omega` tactic to prove `¬(sizeOf lit.lhs = sizeOf lit.rhs)`
+          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body $ mkApp sizeOfEqFalseMVar sizeOfEq -- Has the type `body`
+          trace[duper.rule.datatypeAcyclicity] "lit: {lit}, lit.ty: {lit.ty}, sizeOfInst: {sizeOfInst}, abstrLam: {abstrLam}, sizeOfEq: {sizeOfEq}"
+          trace[duper.rule.datatypeAcyclicity] "sizeOfEqFalseMVar: {sizeOfEqFalseMVar}, proofCase: {proofCase}"
+          Meta.mkLambdaFVars #[h] proofCase
+        proofCases := proofCases.push proofCase
+      else -- `lit` is not the equality to be removed
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i h
+        proofCases := proofCases.push proofCase
+    let proof ← orCases (parentLits.map Lit.toExpr) proofCases
+    Meta.mkLambdaFVars xs $ mkApp proof appliedPremise
+
+/-- Implements the acyclicity rules described in section 6.4 of https://arxiv.org/pdf/1611.02908 -/
+def datatypeAcyclicity : MSimpRule := fun c => do
+  let c ← loadClause c
+  for i in [:c.lits.size] do
+    let lit := c.lits[i]!
+    match ← litComparesConstructorSubterms lit with
+    | some side =>
+      if lit.sign then -- `lit` is never true so `lit` can be removed from `c`
+        let res := c.eraseIdx i
+        let yC ← yieldClause res "datatypeAcyclicity" none -- mkDatatypeAcyclicityProof i side
+        trace[duper.rule.datatypeAcyclicity] "datatypeAcyclicity applied to {c.lits} to yield {yC.1}"
+        return some #[yC]
+      else -- `lit` is a tautology so the clause `c` can simply be removed
+        trace[duper.rule.datatypeAcyclicity] "datatypeAcyclicity applied to remove {c.lits}"
+        return some #[]
+    | none => continue
+  return none

Duper/Rules/DatatypeDistinctness.lean

@@ -0,0 +1,99 @@
+import Duper.Simp
+import Duper.Util.ProofReconstruction
+
+namespace Duper
+open Std
+open RuleM
+open SimpResult
+open Lean
+open Meta
+
+initialize Lean.registerTraceClass `duper.rule.datatypeDistinctness
+
+/-- Returns `none` if `lit` does not compare distinct constructors, returns `some false` if `lit` says two distinct
+    constructors are equal, and returns `some true` if `lit` says two distinct constructors are not equal. -/
+def litComparesDistinctConstructors (lit : Lit) : MetaM (Option Bool) := do
+  let litTyIsInductive ← matchConstInduct lit.ty.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
+  if litTyIsInductive then
+    trace[duper.rule.datatypeDistinctness] "lit.ty {lit.ty} is an inductive datatype"
+    let lhsCtorOpt ← matchConstCtor lit.lhs.getAppFn' (fun _ => pure none) (fun cval lvls => pure (some (cval, lvls)))
+    let rhsCtorOpt ← matchConstCtor lit.rhs.getAppFn' (fun _ => pure none) (fun cval lvls => pure (some (cval, lvls)))
+    match lhsCtorOpt, rhsCtorOpt with
+    | some lhsCtor, some rhsCtor =>
+      trace[duper.rule.datatypeDistinctness] "Both lit.lhs {lit.lhs} and lit.rhs {lit.rhs} have constructors as heads"
+      if lhsCtor == rhsCtor then return none
+      else return !lit.sign
+    | _, _ => -- `lit` is not comparing two constructors
+      trace[duper.rule.datatypeDistinctness] "Either lit.lhs {lit.lhs} or lit.rhs {lit.rhs} does not have a constructor at its head"
+      return none
+  else -- `lit.ty` is not an inductive datatype so `lit` cannot be comparing distinct constructors
+    trace[duper.rule.datatypeDistinctness] "lit.ty {lit.ty} is not an inductive datatype"
+    return none
+
+def mkDatatypeDistinctnessProof (refs : List (Option Nat)) (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 (parentsLits, appliedPremises, transferExprs) ← instantiatePremises parents premises xs transferExprs
+    let parentLits := parentsLits[0]!
+    let appliedPremise := appliedPremises[0]!
+
+    let mut proofCases : Array Expr := Array.mkEmpty parentLits.size
+    for i in [:parentLits.size] do
+      let lit := parentLits[i]!
+      match ← litComparesDistinctConstructors lit with
+      | some true => -- Throw an error because Dist-S⁻ should have been applied, not Dist-S⁺
+        throwError "mkDistPosProof :: Found a literal {lit} asserting that two distinct constructors are not equal"
+      | some false => -- `lit` equates distinct instructors and should not appear in the final clause `c`
+        let matchConstInductK := (fun ival lvls => pure (some (ival.name, ival.numParams, lvls)))
+        let some (tyName, numParams, lvls) ← matchConstInduct lit.ty.getAppFn' (fun _ => pure none) matchConstInductK
+          | throwError "mkDistPosProof :: Failed to find the inductive datatype corresponding to {lit.ty}"
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          let noConfusionArgs := #[some (mkConst ``False), none, none, some h]
+          -- noConfusion first takes `numParams` arguments for parameters, so we need to add that many `none`s to the front of `noConfusionArgs`
+          let noConfusionArgs := (Array.range numParams).map (fun _ => none) ++ noConfusionArgs
+          let proofCase ← mkAppOptM' (mkConst (.str tyName "noConfusion") (0 :: lvls)) noConfusionArgs
+          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          Meta.mkLambdaFVars #[h] proofCase
+        proofCases := proofCases.push proofCase
+      | none => -- refs[i] should have the value (some j) where parentLits[i] == c[j]
+        match refs[i]! with
+        | none =>
+          throwError "There is a bug in mkDistPosProof (The refs invariant is not satisfied)"
+        | some j =>
+          let proofCase ← Meta.withLocalDeclD `h parentLits[i]!.toExpr fun h => do
+            Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) j h
+          proofCases := proofCases.push proofCase
+    let proof ← orCases (parentLits.map Lit.toExpr) proofCases
+    Meta.mkLambdaFVars xs $ mkApp proof appliedPremise
+
+/-- Implements the Dist-S⁺ and Dist-S⁻ rules described in https://arxiv.org/pdf/1611.02908 -/
+def datatypeDistinctness : MSimpRule := fun c => do
+  let c ← loadClause c
+  /- Spec for newLits and refs:
+     - If c.lits[i] equates distinct constructors (e.g. has the form `f s = g t` where `f` and `g` are constructors),
+       then refs[i] = none
+     - If c.lits[i] does not equate distinct constructors, then refs[i] = some j where newLits[j] = c.lits[i] -/
+  let mut newLits : List Lit := []
+  let mut refs : List (Option Nat) := []
+  for lit in c.lits do
+    match ← litComparesDistinctConstructors lit with
+    | some true => -- Apply Dist-S⁻ rule and delete the clause
+      trace[duper.rule.datatypeDistinctness] "datatypeDistinctness- used to remove {c.lits} (due to lit: {lit})"
+      return some #[]
+    | some false => -- Apply Dist-S⁺ rule and remove `lit` from the clause
+      refs := none :: refs
+    | none =>
+      refs := (some newLits.length) :: refs
+      newLits := lit :: newLits
+  -- To achieve the desired spec for newLits and refs, I must reverse them
+  newLits := newLits.reverse
+  refs := refs.reverse
+  if (newLits.length = c.lits.size) then
+    return none
+  else
+    trace[duper.rule.datatypeDistinctness] "datatypeDistinctness+ applied with the newLits: {newLits}"
+    let yc ← yieldClause (MClause.mk newLits.toArray) "datatypeDistinctness+" (some (mkDatatypeDistinctnessProof refs))
+    return some #[yc]
+
+end Duper