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

fix: bug at subst tactic

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-09 19:25:15 -08:00
parent 472ae6adac
commit c3b2a1da50
2 changed files with 34 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Lean/Meta/Tactic/Subst.lean
View file

@ -32,9 +32,7 @@ withMVarContext mvarId $ do
throwTacticEx `subst mvarId ("'" ++ a ++ "' occurs at" ++ indentExpr b);
aLocalDecl ← getLocalDecl aFVarId;
(vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true;
trace `Meta.Tactic.subst $ fun _ => "revert" ++ Format.line ++ MessageData.ofGoal mvarId;
(twoVars, mvarId) ← introN mvarId 2 [] false;
trace `Meta.Tactic.subst $ fun _ => "intro2" ++ Format.line ++ MessageData.ofGoal mvarId;
let aFVarId := twoVars.get! 0;
let a := mkFVar aFVarId;
let hFVarId := twoVars.get! 1;
@ -56,12 +54,9 @@ withMVarContext mvarId $ do
newVal ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major;
modify $ fun s => { mctx := s.mctx.assignExpr mvarId newVal, .. s };
let mvarId := newMVar.mvarId!;
trace `Meta.Tactic.subst $ fun _ => "subst" ++ Format.line ++ MessageData.ofGoal mvarId;
mvarId ← clear mvarId hFVarId;
mvarId ← clear mvarId aFVarId;
trace `Meta.Tactic.subst $ fun _ => "clear" ++ Format.line ++ MessageData.ofGoal mvarId;
(newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false;
trace `Meta.Tactic.subst $ fun _ => "introN" ++ Format.line ++ MessageData.ofGoal mvarId;
fvarSubst ← pure {FVarSubst . }; -- TODO
pure (fvarSubst, mvarId)
};
@ -79,12 +74,11 @@ withMVarContext mvarId $ do
`newType` is type correct because `h` and `hAux.symm` are definitionally equal by proof irrelevance.
3- Create motive by abstracting `a` and `hAux` in `newType`. -/
hAuxType ← mkEq b a;
(motive, newType) ← withLocalDecl `_h hAuxType BinderInfo.default $ fun hAux => do {
motive ← withLocalDecl `_h hAuxType BinderInfo.default $ fun hAux => do {
hAuxSymm ← mkEqSymm hAux;
/- replace h in type with hAuxSymm -/
let newType := (type.abstract #[h]).instantiate1 hAuxSymm;
motive ← mkLambda #[a, hAux] newType;
pure (motive, newType)
mkLambda #[a, hAux] newType
};
continue motive newType
else do

32
tests/lean/run/subst1.lean Normal file
View file

@ -0,0 +1,32 @@
new_frontend
set_option trace.Meta.Tactic.subst true
theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z :=
begin
intros h1 h2 h3;
subst x;
assumption
end
theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z :=
begin
intros h1 h2;
subst h1;
subst h2;
exact rfl
end
def BV (n : Nat) : Type := Unit
theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1) w :=
begin
subst h1;
apply h2
end
theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w :=
begin
subst n;
apply h2
end