Skip to content

Commit d518bbf

Browse files
vasnesterovvasnesterov
committed
partial trimming
1 parent 70a3878 commit d518bbf

15 files changed

Lines changed: 491 additions & 708 deletions

File tree

‎Mathlib/Tactic/Tendsto/Meta/ElimDestruct.lean‎

Lines changed: 33 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -117,43 +117,39 @@ def simpWith (pf : Expr) : SimpM Simp.Step := do
117117
return .visit {expr := rhs, proof? := pf}
118118

119119
simproc elimDestruct (Stream'.Seq.destruct _) := fun e => do
120-
match e.getAppFnArgs with
121-
| (``Stream'.Seq.destruct, #[_, target]) =>
122-
let ⟨1, targetType, target⟩ := ← inferTypeQ target | return .continue
123-
match targetType with
124-
| ~q(PreMS.LazySeries) =>
125-
match target with
126-
| ~q(PreMS.invSeries') =>
127-
simpWith q(invSeries'_destruct)
128-
| _ => return .continue
129-
| ~q(PreMS $basis) =>
130-
match basis with
131-
| ~q(List.cons $basis_hd $basis_tl) =>
132-
match target with
133-
| ~q(PreMS.nil) =>
134-
return .done {
135-
expr := q(@Option.none (Seq1 (ℝ × PreMS $basis_tl))),
136-
proof? := q(@Stream'.Seq.destruct_nil (ℝ × (PreMS $basis_tl)))
137-
}
138-
| ~q(PreMS.cons $hd $tl) =>
139-
return .done {
140-
expr := q(Option.some ($hd, $tl)),
141-
proof? := q(Stream'.Seq.destruct_cons $hd $tl)
142-
}
143-
| ~q(PreMS.const _ $c) => simpWith q(@const_destruct $basis_hd $basis_tl $c)
144-
| ~q(PreMS.monomial _ $n) =>
145-
match (← getNatValue? n).get! with
146-
| 0 => simpWith q(@monomial_zero_destruct $basis_hd $basis_tl)
147-
| m + 1 => simpWith q(@monomial_succ_destruct $basis_hd $basis_tl $m)
148-
| ~q(PreMS.neg $arg) => simpWith q(neg_destruct $arg)
149-
| ~q(PreMS.add $arg1 $arg2) => simpWith q(add_destruct $arg1 $arg2)
150-
| ~q(PreMS.mul $arg1 $arg2) => simpWith q(mul_destruct $arg1 $arg2)
151-
| ~q(PreMS.mulMonomial $b $m_coef $m_exp) =>
152-
simpWith q(mulMonomial_destruct $b $m_coef $m_exp)
153-
| ~q(PreMS.LazySeries.apply $s $ms) => simpWith q(apply_destruct $s $ms)
154-
| ~q(PreMS.inv' $arg) => simpWith q(inv'_destruct $arg)
155-
| _ => return .continue
156-
| _ => return .continue
120+
let (``Stream'.Seq.destruct, #[_, target]) := e.getAppFnArgs | return .continue
121+
let ⟨1, targetType, target⟩ := ← inferTypeQ target | return .continue
122+
match targetType with
123+
| ~q(PreMS.LazySeries) =>
124+
match target with
125+
| ~q(PreMS.invSeries') =>
126+
simpWith q(invSeries'_destruct)
127+
| _ => return .continue
128+
| ~q(PreMS $basis) =>
129+
let ~q(List.cons $basis_hd $basis_tl) := basis | return .continue
130+
match target with
131+
| ~q(PreMS.nil) =>
132+
return .done {
133+
expr := q(@Option.none (Seq1 (ℝ × PreMS $basis_tl))),
134+
proof? := q(@Stream'.Seq.destruct_nil (ℝ × (PreMS $basis_tl)))
135+
}
136+
| ~q(PreMS.cons $hd $tl) =>
137+
return .done {
138+
expr := q(Option.some ($hd, $tl)),
139+
proof? := q(Stream'.Seq.destruct_cons $hd $tl)
140+
}
141+
| ~q(PreMS.const _ $c) => simpWith q(@const_destruct $basis_hd $basis_tl $c)
142+
| ~q(PreMS.monomial _ $n) =>
143+
match (← getNatValue? n).get! with
144+
| 0 => simpWith q(@monomial_zero_destruct $basis_hd $basis_tl)
145+
| m + 1 => simpWith q(@monomial_succ_destruct $basis_hd $basis_tl $m)
146+
| ~q(PreMS.neg $arg) => simpWith q(neg_destruct $arg)
147+
| ~q(PreMS.add $arg1 $arg2) => simpWith q(add_destruct $arg1 $arg2)
148+
| ~q(PreMS.mul $arg1 $arg2) => simpWith q(mul_destruct $arg1 $arg2)
149+
| ~q(PreMS.mulMonomial $b $m_coef $m_exp) =>
150+
simpWith q(mulMonomial_destruct $b $m_coef $m_exp)
151+
| ~q(PreMS.LazySeries.apply $s $ms) => simpWith q(apply_destruct $s $ms)
152+
| ~q(PreMS.inv' $arg) => simpWith q(inv'_destruct $arg)
157153
| _ => return .continue
158154
| _ => return .continue
159155

‎Mathlib/Tactic/Tendsto/Meta/LeadingTerm.lean‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -8,47 +8,47 @@ open Lean Meta Elab Tactic Qq
88
namespace TendstoTactic
99

1010
/-- Given `ms`, computes its leading term `t`. -/
11-
partial def getLeadingTerm {basis : Q(Basis)} (ms : Q(PreMS $basis)) : MetaM Q(MS.Term) := do
11+
partial def getLeadingTerm {basis : Q(Basis)} (ms : Q(PreMS $basis)) : MetaM Q(Term) := do
1212
match basis with
1313
| ~q(List.nil) =>
1414
return q(⟨$ms, List.nil⟩)
1515
| ~q(List.cons $basis_hd $basis_tl) =>
1616
match ms with
1717
| ~q(PreMS.nil) =>
1818
throwError "Unexpected ms = nil in getLeadingTerm"
19-
| ~q(PreMS.cons $hd $tl) =>
20-
match hd with
21-
| ~q(($exp, $coef)) =>
22-
match ← getLeadingTerm coef with
23-
| ~q(⟨$coef_coef, $coef_exps⟩) =>
24-
return q(⟨$coef_coef, $exp :: $coef_exps⟩)
25-
| _ => throwError "Unexpected pre in getLeadingTerm"
26-
| _ => throwError "Unexpected head in getLeadingTerm"
19+
| ~q(PreMS.cons ($exp, $coef) $tl) =>
20+
match ← getLeadingTerm coef with
21+
| ~q(⟨$coef_coef, $coef_exps⟩) =>
22+
return q(⟨$coef_coef, $exp :: $coef_exps⟩)
23+
| _ =>
24+
dbg_trace "Unexpected pre in getLeadingTerm"
25+
return q(⟨Term.coef (PreMS.leadingTerm $coef), $exp :: Term.exps (PreMS.leadingTerm $coef)⟩)
2726
| _ => throwError "Unexpected ms in getLeadingTerm"
27+
| _ => throwError "Unexpected basis in getLeadingTerm"
2828

2929
def getLeadingTermWithProof {basis : Q(Basis)} (ms : Q(PreMS $basis)) :
30-
MetaM ((t : Q(MS.Term)) × Q(PreMS.leadingTerm $ms = $t)) := do
30+
MetaM ((t : Q(Term)) × Q(PreMS.leadingTerm $ms = $t)) := do
3131
let rhs ← getLeadingTerm ms
3232
let e ← mkFreshExprMVar q(PreMS.leadingTerm $ms = $rhs)
3333
e.mvarId!.applyRfl
3434
return ⟨rhs, e⟩
3535

3636
inductive FirstIsResult (x : Q(List ℝ))
37-
| zero (pf : Q(MS.Term.AllZero $x))
38-
| pos (pf : Q(MS.Term.FirstIsPos $x))
39-
| neg (pf : Q(MS.Term.FirstIsNeg $x))
37+
| zero (pf : Q(Term.AllZero $x))
38+
| pos (pf : Q(Term.FirstIsPos $x))
39+
| neg (pf : Q(Term.FirstIsNeg $x))
4040

4141
partial def getFirstIs (x : Q(List ℝ)) : TacticM (FirstIsResult x) := do
4242
match x with
43-
| ~q(List.nil) => return .zero q(MS.Term.AllZero_of_nil)
43+
| ~q(List.nil) => return .zero q(Term.AllZero_of_nil)
4444
| ~q(List.cons $hd $tl) =>
4545
match ← compareReal hd with
46-
| .pos h_hd => return .pos q(MS.Term.FirstIsPos_of_head $tl $h_hd)
47-
| .neg h_hd => return .neg q(MS.Term.FirstIsNeg_of_head $tl $h_hd)
46+
| .pos h_hd => return .pos q(Term.FirstIsPos_of_head $tl $h_hd)
47+
| .neg h_hd => return .neg q(Term.FirstIsNeg_of_head $tl $h_hd)
4848
| .zero h_hd =>
4949
return match ← getFirstIs tl with
50-
| .zero h_tl => .zero q(MS.Term.AllZero_of_tail $h_hd $h_tl)
51-
| .pos h_tl => .pos q(MS.Term.FirstIsPos_of_tail $h_hd $h_tl)
52-
| .neg h_tl => .neg q(MS.Term.FirstIsNeg_of_tail $h_hd $h_tl)
50+
| .zero h_tl => .zero q(Term.AllZero_of_tail $h_hd $h_tl)
51+
| .pos h_tl => .pos q(Term.FirstIsPos_of_tail $h_hd $h_tl)
52+
| .neg h_tl => .neg q(Term.FirstIsNeg_of_tail $h_hd $h_tl)
5353

5454
end TendstoTactic

‎Mathlib/Tactic/Tendsto/Meta/MS.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,11 @@ structure MS where
1010
F : Q(ℝ → ℝ)
1111
h_wo : Q(PreMS.WellOrdered $val)
1212
h_approx : Q(PreMS.Approximates $val $F)
13-
h_basis : Q(MS.WellOrderedBasis $basis)
13+
h_basis : Q(WellOrderedBasis $basis)
1414

1515
namespace MS
1616

17-
def const (basis : Q(Basis)) (c : Q(ℝ)) (h_basis : Q(MS.WellOrderedBasis $basis)) : MS where
17+
def const (basis : Q(Basis)) (c : Q(ℝ)) (h_basis : Q(WellOrderedBasis $basis)) : MS where
1818
basis := basis
1919
val := q(PreMS.const $basis $c)
2020
F := q(fun _ ↦ $c)
@@ -23,7 +23,7 @@ def const (basis : Q(Basis)) (c : Q(ℝ)) (h_basis : Q(MS.WellOrderedBasis $basi
2323
h_basis := h_basis
2424

2525
def monomial (basis : Q(Basis)) (n : ℕ) (h : Q($n < List.length $basis))
26-
(h_basis : Q(MS.WellOrderedBasis $basis)) : MS where
26+
(h_basis : Q(WellOrderedBasis $basis)) : MS where
2727
basis := basis
2828
val := q(PreMS.monomial $basis $n)
2929
F := q(List.get $basis ⟨$n, $h⟩)

‎Mathlib/Tactic/Tendsto/Meta/Main.lean‎

Lines changed: 48 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -4,21 +4,21 @@ import Mathlib.Tactic.Tendsto.Meta.LeadingTerm
44

55
set_option linter.style.longLine false
66

7-
open Filter Asymptotics TendstoTactic Stream' Seq ElimDestruct
7+
open Filter Asymptotics TendstoTactic Stream'.Seq ElimDestruct
88

99
open Lean Elab Meta Tactic Qq
1010

1111
namespace TendstoTactic
1212

13-
def basis_wo : MS.WellOrderedBasis [fun (x : ℝ) ↦ x] := by
14-
simp [MS.WellOrderedBasis]
13+
def basis_wo : WellOrderedBasis [fun (x : ℝ) ↦ x] := by
14+
simp [WellOrderedBasis]
1515
exact fun ⦃U⦄ a ↦ a
1616

1717
partial def createMS (body : Expr) : TacticM MS := do
1818
let basis : Q(List (ℝ → ℝ)) := q([fun (x : ℝ) ↦ x])
19-
let basis_wo : Q(MS.WellOrderedBasis $basis) := q(basis_wo)
19+
let basis_wo : Q(WellOrderedBasis $basis) := q(basis_wo)
2020
let zero_aux : Q(0 < List.length $basis) := q(by decide)
21-
match body.nat? with
21+
match body.nat? with -- TODO: other numerals
2222
| .some n =>
2323
return MS.const basis body basis_wo
2424
| none =>
@@ -54,89 +54,63 @@ partial def createMS (body : Expr) : TacticM MS := do
5454
return MS.div ms1 ms2 h_trimmed ⟨⟩
5555
| _ => throwError f!"Unsupported body in createMS: {body}"
5656

57+
5758
def computeTendsto (f : Q(ℝ → ℝ)) : TacticM ((limit : Q(Filter ℝ)) × Q(Tendsto $f atTop $limit)) := do
5859
match f with
5960
| .lam _ _ b _ =>
6061
let ms ← createMS b
61-
let ⟨ms_trimmed, h_trimmed⟩ ← trimMS ms
62+
let ⟨ms_trimmed, h_trimmed⟩ ← trimPartialMS ms
6263

6364
let hf_eq ← mkFreshExprMVarQ q($ms.F = $f)
6465
hf_eq.mvarId!.applyRfl
6566

66-
let limit ← mkFreshExprMVarQ q(Filter ℝ)
67-
let goal ← mkFreshExprMVarQ q(Tendsto $ms.F atTop $limit)
68-
let targetType := Q(Tendsto $f atTop $limit)
69-
let res : targetType := q(Eq.subst (motive := fun x ↦ Tendsto x atTop $limit) $hf_eq $goal)
70-
71-
match ms_trimmed.basis with
72-
| ~q(List.cons $basis_hd $basis_tl) =>
73-
match ms_trimmed.val with
74-
| ~q(PreMS.nil) =>
75-
limit.mvarId!.assign q(nhds (0 : ℝ))
76-
let h_tendsto := q(PreMS.nil_tendsto_zero $ms_trimmed.h_approx)
77-
goal.mvarId!.assign h_tendsto
78-
| ~q(PreMS.cons $hd $tl) =>
79-
let ⟨leading, h_leading_eq⟩ ← getLeadingTermWithProof ms_trimmed.val
80-
let h_tendsto ← match leading with
81-
| ~q(⟨$coef, $exps⟩) =>
82-
let coef_comp ← compareReal coef
83-
match coef_comp with
84-
| .zero h_coef =>
85-
limit.mvarId!.assign q(nhds (0 : ℝ))
86-
return q(PreMS.tendsto_zero_of_zero_coef $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_coef)
87-
| .neg h_coef =>
88-
match ← getFirstIs exps with
89-
| .pos h_exps =>
90-
return q(PreMS.tendsto_bot_of_FirstIsPos $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_exps $h_coef)
91-
| .neg h_exps =>
92-
return q(PreMS.tendsto_zero_of_FirstIsNeg $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_exps)
93-
| .zero h_exps =>
94-
return q(PreMS.tendsto_const_of_AllZero $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_exps)
95-
| .pos h_coef =>
96-
match ← getFirstIs exps with
97-
| .pos h_exps =>
98-
return q(PreMS.tendsto_top_of_FirstIsPos $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_exps $h_coef)
99-
| .neg h_exps =>
100-
return q(PreMS.tendsto_zero_of_FirstIsNeg $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_exps)
101-
| .zero h_exps =>
102-
return q(PreMS.tendsto_const_of_AllZero $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed $ms_trimmed.h_basis $h_leading_eq $h_exps)
103-
| _ => throwError "Unexpected result of getLeadingTermWithProof"
104-
goal.mvarId!.assign h_tendsto
105-
| _ => throwError "Unexpected result of trimMS"
106-
| _ => throwError "Unexpected basis in computeTendsto"
67+
let ~q(List.cons $basis_hd $basis_tl) := ms_trimmed.basis | throwError "Unexpected basis in computeTendsto"
68+
-- I don't how to avoid Expr here.
69+
let h_tendsto : Expr ← match ms_trimmed.val with
70+
| ~q(PreMS.nil) =>
71+
pure (q(PreMS.nil_tendsto_zero $ms_trimmed.h_approx) : Expr)
72+
| ~q(PreMS.cons $hd $tl) =>
73+
let ⟨leading, h_leading_eq⟩ ← getLeadingTermWithProof ms_trimmed.val
74+
let ~q(⟨$coef, $exps⟩) := leading | throwError "Unexpected leading in computeTendsto"
75+
let h_tendsto ← match ← getFirstIs exps with
76+
| .pos h_exps =>
77+
match ← compareReal coef with
78+
| .neg h_coef =>
79+
pure (q(PreMS.tendsto_bot_of_FirstIsPos $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed.get! $ms_trimmed.h_basis $h_leading_eq $h_exps $h_coef) : Expr)
80+
| .pos h_coef =>
81+
pure (q(PreMS.tendsto_top_of_FirstIsPos $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed.get! $ms_trimmed.h_basis $h_leading_eq $h_exps $h_coef) : Expr)
82+
| .zero _ => throwError "Unexpected zero coef with FirstIsPos"
83+
| .neg h_exps =>
84+
pure (q(PreMS.tendsto_zero_of_FirstIsNeg $ms_trimmed.h_wo $ms_trimmed.h_approx $h_leading_eq $h_exps) : Expr)
85+
| .zero h_exps =>
86+
pure (q(PreMS.tendsto_const_of_AllZero $ms_trimmed.h_wo $ms_trimmed.h_approx $h_trimmed.get! $ms_trimmed.h_basis $h_leading_eq $h_exps) : Expr)
87+
| _ => throwError "Unexpected result of trimMS"
10788

108-
-- TODO: is this necessary?
109-
let goal' ← instantiateMVarsQ goal
110-
let ⟨0, t, _⟩ ← inferTypeQ goal' | throwError "Unexpected goal's universe level"
111-
match t with
112-
| ~q(Tendsto (α := ℝ) (β := ℝ) $f atTop $limit_res) =>
113-
limit.mvarId!.assign limit_res
114-
| _ => pure ()
89+
let ⟨0, t, h_tendsto⟩ ← inferTypeQ h_tendsto | throwError "Unexpected h_tendsto's universe level"
90+
let ~q(@Tendsto ℝ ℝ $g atTop $limit) := t | throwError "Unexpected h_tendsto's type"
91+
haveI' : $g =Q $ms.F := ⟨⟩
11592

116-
return ⟨← instantiateMVarsQ limit, ← instantiateMVars res⟩
93+
let res := q(Eq.subst (motive := fun x ↦ Tendsto x atTop $limit) $hf_eq $h_tendsto)
94+
return ⟨limit, res⟩
11795
| _ => throwError "Function should be lambda"
11896

11997
elab "compute_asymptotics" : tactic =>
12098
Lean.Elab.Tactic.withMainContext do
12199
let target : Q(Prop) ← getMainTarget
122-
match target with
123-
| ~q(@Filter.Tendsto ℝ ℝ $f atTop $targetLimit) =>
124-
let ⟨1, fType, f⟩ ← inferTypeQ f | throwError "Unexpected universe level of function in compute_asymptotics"
125-
match fType with
126-
| ~q(ℝ → ℝ) =>
127-
let ⟨limit, h_tendsto⟩ ← computeTendsto f
128-
let result : Q(Prop) ← inferType h_tendsto
129-
if !(← isDefEq target result) then
130-
match targetLimit, limit with
131-
| ~q(nhds $a), ~q(nhds $b) =>
132-
let h_eq : Q($b = $a) ← mkFreshExprMVarQ q($b = $a)
133-
(← getMainGoal).assign q(Eq.subst (motive := fun x ↦ Filter.Tendsto $f atTop (nhds (X := ℝ) x)) $h_eq $h_tendsto)
134-
setGoals (← evalTacticAt (← `(tactic| try norm_num1)) h_eq.mvarId!)
135-
| _ =>
136-
throwError m!"I've proved that {← ppExpr (← inferType h_tendsto)}. Is this what you expect?"
137-
else
138-
(← getMainGoal).assign h_tendsto
139-
| _ => throwError "Only real functions are supported"
140-
| _ => throwError "The goal must me in the form Tendsto (fun x ↦ ...) atTop ..."
100+
let ~q(@Filter.Tendsto ℝ ℝ $f atTop $targetLimit) := target | throwError "The goal must me in the form Tendsto (fun x ↦ ...) atTop ..."
101+
let ⟨1, fType, f⟩ ← inferTypeQ f | throwError "Unexpected universe level of function in compute_asymptotics"
102+
let ~q(ℝ → ℝ) := fType | throwError "Only real functions are supported"
103+
let ⟨limit, h_tendsto⟩ ← computeTendsto f
104+
let result : Q(Prop) ← inferType h_tendsto
105+
if !(← isDefEq target result) then
106+
match targetLimit, limit with
107+
| ~q(nhds $a), ~q(nhds $b) =>
108+
let h_eq : Q($b = $a) ← mkFreshExprMVarQ q($b = $a)
109+
(← getMainGoal).assign q(Eq.subst (motive := fun x ↦ Filter.Tendsto $f atTop (nhds (X := ℝ) x)) $h_eq $h_tendsto)
110+
setGoals (← evalTacticAt (← `(tactic| try norm_num1)) h_eq.mvarId!)
111+
| _ =>
112+
throwError m!"I've proved that {← ppExpr (← inferType h_tendsto)}. Is this what you expect?"
113+
else
114+
(← getMainGoal).assign h_tendsto
141115

142116
end TendstoTactic

0 commit comments

Comments
 (0)