From 530b94e022dca0c38b8331285ddd86bb2c788701 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 17:09:21 -0500 Subject: [PATCH] Added support for facts whose types are not Prop but can be made definitionally equal to Prop with metavariable assignment --- Duper/Tactic.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 744e236..54e4b13 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -172,6 +172,13 @@ def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Ar if ← isProp fact then let fact ← preprocessFact (← instantiateMVars fact) formulas := (fact, ← mkAppM ``eq_true #[proof], params, false, some factStx) :: formulas + else if ← isDefEq (← inferType fact) (.sort 0) then + /- This check can succeed where the previous failed in instances where `fact`'s type is + a sort with an undetermined universe level. We try the previous check first to avoid + unnecessarily assigning metavariables in `fact`'s type (which the above `isDefEq` check + can do)-/ + let fact ← preprocessFact (← instantiateMVars fact) + formulas := (fact, ← mkAppM ``eq_true #[proof], params, false, some factStx) :: formulas else if ← getIgnoreUnusableFactsM then trace[duper.ignoredUnusableFacts] "Ignored {fact} ({factStx}) because it is not a Prop" continue