Skip to content

Commit

Permalink
projection rule in fprop
Browse files Browse the repository at this point in the history
  • Loading branch information
lecopivo committed Jul 27, 2023
1 parent 90ab448 commit 4534a91
Show file tree
Hide file tree
Showing 7 changed files with 147 additions and 8 deletions.
24 changes: 21 additions & 3 deletions SciLean/FTrans/Adjoint/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -100,18 +100,36 @@ by
rw[h']; rfl


#exit

example : CompleteSpace ((i :ι) → E i) := by infer_instance

open BigOperators

set_option trace.Meta.Tactic.fprop.discharge true in
-- set_option trace.Meta.Tactic.fprop.discharge true in
-- set_option trace.Meta.Tactic.fprop.step true in
theorem pi_rule
(x : X)
(f : (i : ι) → X → E i) (hf : ∀ i, IsContinuousLinearMap K (f i))
: ((fun (x : X) =>L[K] fun (i : ι) => f i x) : X →L[K] PiLp 2 E)†
=
(fun x' =>L[K] ∑ i, (fun x =>L[K] f i x)† (x' i))
:= sorry


set_option trace.Meta.Tactic.fprop.discharge true in
-- theorem proj_rule [DecidableEq ι]
-- (i : ι)
-- : (fun (f : PiLp 2 E) =>L[K] f i)†
-- =
-- fun y =>L[K] ((fun j => if h : i=j then (h ▸ y) else (0 : E j)) : PiLp 2 E)
-- := sorry

theorem proj_rule [DecidableEq ι]
(i : ι)
: (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)†
=
fun x =>L[K] (fun j => if h : i=j then x else (0 : X))
:= sorry




14 changes: 14 additions & 0 deletions SciLean/FunctionSpaces/Continuous/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,11 @@ theorem pi_rule
: Continuous (fun x i => f i x)
:= by continuity

theorem proj_rule
(i : ι)
: Continuous (fun x : (i : ι) → E i => x i)
:= by continuity


end SciLean.Continuous

Expand Down Expand Up @@ -143,6 +148,15 @@ def Continuous.fpropExt : FPropExt where
}
FProp.tryTheorem? e thm (fun _ => pure none)

projRule e :=
let thm : SimpTheorem :=
{
proof := mkConst ``Continuous.proj_rule
origin := .decl ``Continuous.proj_rule
rfl := false
}
FProp.tryTheorem? e thm (fun _ => pure none)

discharger _ := return none

-- register fderiv
Expand Down
51 changes: 48 additions & 3 deletions SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -103,10 +103,16 @@ theorem pi_rule
(by simp)


theorem proj_rule (i : ι)
: IsContinuousLinearMap R fun f : (i : ι) → E i => f i
:=
by_morphism (ContinuousLinearMap.proj i) (by simp)


end SciLean.IsContinuousLinearMap

--------------------------------------------------------------------------------
-- Register Diferentiable ------------------------------------------------------
-- Register IsContinuousLinearMap ----------------------------------------------
--------------------------------------------------------------------------------

open Lean Meta SciLean FProp
Expand Down Expand Up @@ -194,6 +200,16 @@ def IsContinuousLinearMap.fpropExt : FPropExt where
}
FProp.tryTheorem? e thm (fun _ => pure none)

projRule e :=
let thm : SimpTheorem :=
{
proof := mkConst ``IsContinuousLinearMap.proj_rule
origin := .decl ``IsContinuousLinearMap.proj_rule
rfl := false
}
FProp.tryTheorem? e thm (fun _ => pure none)


discharger _ := return none

-- register fderiv
Expand Down Expand Up @@ -486,12 +502,16 @@ theorem HDiv.hDul.arg_a4.IsContinuousLinearMap_comp
-- Finset.sum -------------------------------------------------------------------
--------------------------------------------------------------------------------


open BigOperators in
@[fprop_rule]
theorem Finset.sum.arg_f.IsContinuousLinearMap_comp
(f : X → ι → Y) (hf : ∀ i, IsContinuousLinearMap R fun x : X => f x i) (A : Finset ι)
: IsContinuousLinearMap R fun x => ∑ i in A, f x i := sorry
: IsContinuousLinearMap R fun x => ∑ i in A, f x i :=
{
map_add' := sorry
map_smul' := sorry
cont := sorry
}

-- do we need this one?
-- open BigOperators in
Expand All @@ -500,3 +520,28 @@ theorem Finset.sum.arg_f.IsContinuousLinearMap_comp
-- (f : ι → X → Y) (hf : ∀ i, IsContinuousLinearMap R (f i)) (A : Finset ι)
-- : IsContinuousLinearMap R fun (x : X) => ∑ i in A, f i x := sorry


-- ite -------------------------------------------------------------------------
--------------------------------------------------------------------------------

@[fprop_rule]
theorem ite.arg_te.IsContinuousLinearMap_comp
(c : Prop) [dec : Decidable c]
(t e : X → Y) (ht : IsContinuousLinearMap R t) (he : IsContinuousLinearMap R e)
: IsContinuousLinearMap R fun x => ite c (t x) (e x) :=
by
induction dec
case isTrue h => simp[h]; fprop
case isFalse h => simp[h]; fprop


@[fprop_rule]
theorem dite.arg_te.IsContinuousLinearMap_comp
(c : Prop) [dec : Decidable c]
(t : c → X → Y) (ht : ∀ p, IsContinuousLinearMap R (t p))
(e : ¬c → X → Y) (he : ∀ p, IsContinuousLinearMap R (e p))
: IsContinuousLinearMap R fun x => dite c (t · x) (e · x) :=
by
induction dec
case isTrue h => simp[h]; apply ht
case isFalse h => simp[h]; apply he
15 changes: 15 additions & 0 deletions SciLean/FunctionSpaces/Differentiable/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,11 @@ theorem pi_rule
: Differentiable R (fun x i => f i x)
:= fun x => DifferentiableAt.pi_rule x f (fun i => hf i x)

theorem proj_rule
(i : ι)
: Differentiable R (fun x : (i : ι) → E i => x i):=
by
apply DifferentiableAt.proj_rule


end SciLean.Differentiable
Expand Down Expand Up @@ -155,6 +160,16 @@ def Differentiable.fpropExt : FPropExt where
}
FProp.tryTheorem? e thm (fun _ => pure none)

projRule e :=
let thm : SimpTheorem :=
{
proof := mkConst ``DifferentiableAt.proj_rule
origin := .decl ``DifferentiableAt.proj_rule
rfl := false
}
FProp.tryTheorem? e thm (fun _ => pure none)


discharger _ := return none

-- register fderiv
Expand Down
18 changes: 18 additions & 0 deletions SciLean/FunctionSpaces/DifferentiableAt/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import Mathlib.Analysis.Calculus.Deriv.Inv
import SciLean.Tactic.FProp.Basic
import SciLean.Tactic.FProp.Notation

import SciLean.FunctionSpaces.ContinuousLinearMap.Notation

namespace SciLean

Expand Down Expand Up @@ -65,6 +66,14 @@ theorem pi_rule
:= by apply differentiableAt_pi.2 hf


theorem proj_rule
(i : ι) (x)
: DifferentiableAt R (fun x : (i : ι) → E i => x i) x :=
by
apply IsBoundedLinearMap.differentiableAt
apply ContinuousLinearMap.isBoundedLinearMap (fun (x : (i : ι) → E i) =>L[R] x i)


end SciLean.DifferentiableAt


Expand Down Expand Up @@ -162,6 +171,15 @@ def DifferentiableAt.fpropExt : FPropExt where
}
FProp.tryTheorem? e thm (fun _ => pure none)

projRule e :=
let thm : SimpTheorem :=
{
proof := mkConst ``DifferentiableAt.proj_rule
origin := .decl ``DifferentiableAt.proj_rule
rfl := false
}
FProp.tryTheorem? e thm (fun _ => pure none)

discharger e :=
FProp.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption") e

Expand Down
31 changes: 29 additions & 2 deletions SciLean/Tactic/FProp/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,31 @@ def tacticToDischarge (tacticCode : Syntax) : Expr → MetaM (Option Expr) := fu

return result?

def applyBVarApp (e : Expr) : FPropM (Option Expr) := do
let .some (fpropName, ext, F) ← getFProp? e
| return none

let .lam n t (.app f x) bi := F
| trace[Meta.Tactic.fprop.step] "bvar app step can't handle functions like {← ppExpr F}"
return none

if x.hasLooseBVars then
trace[Meta.Tactic.fprop.step] "bvar app step can't handle functions like {← ppExpr F}"
return none


if f == .bvar 0 then
ext.projRule e
else
let g := .lam n t f bi
let gType ← inferType g
let fType := gType.getForallBody
if fType.hasLooseBVars then
trace[Meta.Tactic.fprop.step] "bvar app step can't handle dependent functions of type {← ppExpr fType} appearing in {← ppExpr F}"
return none

let h := .lam n fType ((Expr.bvar 0).app x) bi
ext.compRule e h g

/-- Takes lambda function `fun x => b` and splits it into composition of two functions.
Expand Down Expand Up @@ -163,6 +188,9 @@ mutual
else if b.getAppFn.isFVar then
trace[Meta.Tactic.fprop.step] "case fvar app\n{← ppExpr e}"
applyFVarApp e ext.discharger
else if b.getAppFn.isBVar then
trace[Meta.Tactic.fprop.step] "case bvar app\n{← ppExpr e}"
applyBVarApp e
else
trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}\n"
applyTheorems e (ext.discharger)
Expand Down Expand Up @@ -212,8 +240,7 @@ mutual
if let some proof ← tryTheorem? e thm discharge? then
return proof

return none -- ext.lambdaLetRule e
-- return none
return none

partial def synthesizeInstance (thmId : Origin) (x type : Expr) : MetaM Bool := do
match (← trySynthInstance type) with
Expand Down
2 changes: 2 additions & 0 deletions SciLean/Tactic/FProp/Init.lean
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@ structure _root_.SciLean.FPropExt where
identityRule (expr : Expr) : FPropM (Option Expr)
/-- Custom rule for proving property of `fun x => y -/
constantRule (expr : Expr) : FPropM (Option Expr)
/-- Custom rule for proving property of `fun x => x i -/
projRule (expr : Expr) : FPropM (Option Expr)
/-- Custom rule for proving property of `fun x => f (g x)` or `fun x => let y := g x; f y` -/
compRule (expr f g : Expr) : FPropM (Option Expr)
/-- Custom rule for proving property of `fun x => let y := g x; f x y -/
Expand Down

0 comments on commit 4534a91

Please sign in to comment.