max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-17 08:02:30 -07:00
parent f0bc72c2c1
commit 152f275aac
1 changed files with 37 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

74
src/Lean/Meta/Tactic/Injection.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -8,41 +9,40 @@ import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.Intro
namespace Lean
namespace Meta
namespace Lean.Meta
inductive InjectionResultCore
| solved
| subgoal (mvarId : MVarId) (numNewEqs : Nat)
def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCore := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `injection;
decl ← getLocalDecl fvarId;
type ← whnf decl.type;
def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCore :=
withMVarContext mvarId do
checkNotAssigned mvarId `injection
let decl ← getLocalDecl fvarId
let type ← whnf decl.type
match type.eq? with
| none => throwTacticEx `injection mvarId "equality expected"
| some (α, a, b) => do
a ← whnf a;
b ← whnf b;
target ← getMVarType mvarId;
env ← getEnv;
| some (α, a, b) =>
let a ← whnf a
let b ← whnf b
let target ← getMVarType mvarId
let env ← getEnv
match a.isConstructorApp? env, b.isConstructorApp? env with
| some aCtor, some bCtor => do
val ← mkNoConfusion target (mkFVar fvarId);
if aCtor.name != bCtor.name then do
assignExprMVar mvarId val;
| some aCtor, some bCtor =>
let val ← mkNoConfusion target (mkFVar fvarId)
if aCtor.name != bCtor.name then
assignExprMVar mvarId val
pure InjectionResultCore.solved
else do
valType ← inferType val;
valType ← whnf valType;
let valType ← inferType val
let valType ← whnf valType
match valType with
| Expr.forallE _ newTarget _ _ => do
let newTarget := newTarget.headBeta;
tag ← getMVarTag mvarId;
newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
assignExprMVar mvarId (mkApp val newMVar);
mvarId ← tryClear newMVar.mvarId! fvarId;
| Expr.forallE _ newTarget _ _ =>
let newTarget := newTarget.headBeta
let tag ← getMVarTag mvarId
let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
assignExprMVar mvarId (mkApp val newMVar)
let mvarId ← tryClear newMVar.mvarId! fvarId
pure $ InjectionResultCore.subgoal mvarId aCtor.nfields
| _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
| _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"
@ -52,33 +52,33 @@ inductive InjectionResult
| subgoal (mvarId : MVarId) (newEqs : Array FVarId) (remainingNames : List Name)
private def heqToEq (mvarId : MVarId) (fvarId : FVarId) : MetaM (FVarId × MVarId) :=
withMVarContext mvarId $ do
decl ← getLocalDecl fvarId;
type ← whnf decl.type;
withMVarContext mvarId do
let decl ← getLocalDecl fvarId
let type ← whnf decl.type
match type.heq? with
| none => pure (fvarId, mvarId)
| some (α, a, β, b) => do
pr ← mkEqOfHEq (mkFVar fvarId);
eq ← mkEq a b;
mvarId ← assert mvarId decl.userName eq pr;
mvarId ← clear mvarId fvarId;
(fvarId, mvarId) ← intro1P mvarId;
let pr ← mkEqOfHEq (mkFVar fvarId)
let eq ← mkEq a b
let mvarId ← assert mvarId decl.userName eq pr
let mvarId ← clear mvarId fvarId
let (fvarId, mvarId) ← intro1P mvarId
pure (fvarId, mvarId)
def injectionIntro : Nat → MVarId → Array FVarId → List Name → MetaM InjectionResult
| 0, mvarId, fvarIds, remainingNames =>
pure $ InjectionResult.subgoal mvarId fvarIds remainingNames
| n+1, mvarId, fvarIds, name::remainingNames => do
(fvarId, mvarId) ← intro mvarId name;
(fvarId, mvarId) ← heqToEq mvarId fvarId;
let (fvarId, mvarId) ← intro mvarId name
let (fvarId, mvarId) ← heqToEq mvarId fvarId
injectionIntro n mvarId (fvarIds.push fvarId) remainingNames
| n+1, mvarId, fvarIds, [] => do
(fvarId, mvarId) ← intro1 mvarId;
(fvarId, mvarId) ← heqToEq mvarId fvarId;
let (fvarId, mvarId) ← intro1 mvarId
let (fvarId, mvarId) ← heqToEq mvarId fvarId
injectionIntro n mvarId (fvarIds.push fvarId) []
def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) (useUnusedNames : Bool := true) : MetaM InjectionResult := do
r ← injectionCore mvarId fvarId;
let r ← injectionCore mvarId fvarId
match r with
| InjectionResultCore.solved => pure InjectionResult.solved
| InjectionResultCore.subgoal mvarId numEqs => injectionIntro numEqs mvarId #[] newNames