From b80741ef507080a947039b443d0f43b91a284726 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Mon, 27 Nov 2023 06:16:00 +0100 Subject: [PATCH] revDeriv rules for div, if, inner, norm2, sum --- .../FunctionTransformations/RevDeriv.lean | 493 ++++++++++++++++++ SciLean/Data/StructLike/Algebra.lean | 77 ++- SciLean/Data/StructLike/Basic.lean | 27 +- 3 files changed, 576 insertions(+), 21 deletions(-) diff --git a/SciLean/Core/FunctionTransformations/RevDeriv.lean b/SciLean/Core/FunctionTransformations/RevDeriv.lean index 536aaf69..1c5225a9 100644 --- a/SciLean/Core/FunctionTransformations/RevDeriv.lean +++ b/SciLean/Core/FunctionTransformations/RevDeriv.lean @@ -1383,3 +1383,496 @@ by ftrans; simp[revDerivUpdate,add_assoc] + +-- HDiv.hDiv ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem HDiv.hDiv.arg_a0a1.revDeriv_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0) + : (revDeriv K fun x => f x / g x) + = + fun x => + let ydf := revDeriv K f x + let zdg := revDerivUpdate K g x + (ydf.1 / zdg.1, + fun dx' => (1 / (conj zdg.1)^2) • (zdg.2 (-conj ydf.1 • dx') (conj zdg.1 • ydf.2 dx'))) := +by + have ⟨_,_⟩ := hf + have ⟨_,_⟩ := hg + unfold revDeriv; simp; ftrans; ftrans + simp[revDerivUpdate,smul_push,neg_pull,revDeriv,smul_add,smul_sub, ← sub_eq_add_neg] + +@[ftrans] +theorem HDiv.hDiv.arg_a0a1.revDerivUpdate_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0) + : (revDerivUpdate K fun x => f x / g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revDerivUpdate K g x + (ydf.1 / zdg.1, + fun dx' dx => + let c := (1 / (conj zdg.1)^2) + let a := -(c * conj ydf.1) + let b := c * conj zdg.1 + ((zdg.2 (a • dx') (ydf.2 (b • dx') dx)))) := +by + simp[revDerivUpdate]; ftrans + simp[revDerivUpdate,smul_push,neg_pull,revDeriv,smul_add,smul_sub,add_assoc,mul_assoc] + +@[ftrans] +theorem HDiv.hDiv.arg_a0a1.revDerivProj_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0) + : (revDerivProj K fun x => f x / g x) + = + fun x => + let ydf := revDeriv K f x + let zdg := revDerivUpdate K g x + (ydf.1 / zdg.1, + fun _ dx' => (1 / (conj zdg.1)^2) • (zdg.2 (-conj ydf.1 • dx') (conj zdg.1 • ydf.2 dx'))) := +by + unfold revDerivProj + ftrans; simp[StructLike.oneHot, StructLike.make] + +@[ftrans] +theorem HDiv.hDiv.arg_a0a1.revDerivProjUpdate_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0) + : (revDerivProjUpdate K fun x => f x / g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revDerivUpdate K g x + (ydf.1 / zdg.1, + fun _ dx' dx => + let c := (1 / (conj zdg.1)^2) + let a := -(c * conj ydf.1) + let b := c * conj zdg.1 + ((zdg.2 (a • dx') (ydf.2 (b • dx') dx)))) := +by + unfold revDerivProjUpdate + ftrans; simp[revDerivUpdate,revDeriv,add_assoc,neg_pull,mul_assoc,smul_push] + + +-- HPow.hPow ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + + +-- EnumType.sum ---------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem SciLean.EnumType.sum.arg_f.revDeriv_rule {ι : Type} [EnumType ι] + (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i)) + : revDeriv K (fun x => ∑ i, f x i) + = + fun x => + let ydf := revDerivProjUpdate K f x + (∑ i, ydf.1 i, + fun dy => Id.run do + let mut dx := 0 + for i in fullRange ι do + dx := ydf.2 (i,()) dy dx + dx) := +by + have _ := fun i => (hf i).1 + have _ := fun i => (hf i).2 + simp [revDeriv] + funext x; simp + ftrans; ftrans + sorry_proof + + +@[ftrans] +theorem SciLean.EnumType.sum.arg_f.revDerivUpdate_rule {ι : Type} [EnumType ι] + (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i)) + : revDerivUpdate K (fun x => ∑ i, f x i) + = + fun x => + let ydf := revDerivProjUpdate K f x + (∑ i, ydf.1 i, + fun dy dx => Id.run do + let mut dx := dx + for i in fullRange ι do + dx := ydf.2 (i,()) dy dx + dx) := +by + simp[revDerivUpdate] + ftrans + sorry_proof + + +@[ftrans] +theorem SciLean.EnumType.sum.arg_f.revDerivProj_rule {ι : Type} [EnumType ι] + (f : X → ι → Y') (hf : ∀ i, HasAdjDiff K (fun x => f x i)) + : revDerivProj K (fun x => ∑ i, f x i) + = + fun x => + let ydf := revDerivProjUpdate K f x + (∑ i, ydf.1 i, + fun i dy => Id.run do + let mut dx : X := 0 + for j in fullRange ι do + dx := ydf.2 (j,i) dy dx + dx) := +by + simp[revDerivProj]; ftrans; simp; sorry_proof + + +@[ftrans] +theorem SciLean.EnumType.sum.arg_f.revDerivProjUpdate_rule {ι : Type} [EnumType ι] + (f : X → ι → Y') (hf : ∀ i, HasAdjDiff K (fun x => f x i)) + : revDerivProjUpdate K (fun x => ∑ i, f x i) + = + fun x => + let ydf := revDerivProjUpdate K f x + (∑ i, ydf.1 i, + fun i dy dx => Id.run do + let mut dx : X := dx + for j in fullRange ι do + dx := ydf.2 (j,i) dy dx + dx) := +by + simp[revDerivProjUpdate]; ftrans; simp; sorry_proof + + +-- d/ite ----------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem ite.arg_te.revDeriv_rule + (c : Prop) [dec : Decidable c] (t e : X → Y) + : revDeriv K (fun x => ite c (t x) (e x)) + = + fun y => + ite c (revDeriv K t y) (revDeriv K e y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + +@[ftrans] +theorem ite.arg_te.revDerivUpdate_rule + (c : Prop) [dec : Decidable c] (t e : X → Y) + : revDerivUpdate K (fun x => ite c (t x) (e x)) + = + fun y => + ite c (revDerivUpdate K t y) (revDerivUpdate K e y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + +@[ftrans] +theorem ite.arg_te.revDerivProj_rule + (c : Prop) [dec : Decidable c] (t e : X → Y') + : revDerivProj K (fun x => ite c (t x) (e x)) + = + fun y => + ite c (revDerivProj K t y) (revDerivProj K e y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + +@[ftrans] +theorem ite.arg_te.revDerivProjUpdate_rule + (c : Prop) [dec : Decidable c] (t e : X → Y') + : revDerivProjUpdate K (fun x => ite c (t x) (e x)) + = + fun y => + ite c (revDerivProjUpdate K t y) (revDerivProjUpdate K e y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + + +@[ftrans] +theorem dite.arg_te.revDeriv_rule + (c : Prop) [dec : Decidable c] + (t : c → X → Y) (e : ¬c → X → Y) + : revDeriv K (fun x => dite c (t · x) (e · x)) + = + fun y => + dite c (fun p => revDeriv K (t p) y) + (fun p => revDeriv K (e p) y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + +@[ftrans] +theorem dite.arg_te.revDerivUpdate_rule + (c : Prop) [dec : Decidable c] + (t : c → X → Y) (e : ¬c → X → Y) + : revDerivUpdate K (fun x => dite c (t · x) (e · x)) + = + fun y => + dite c (fun p => revDerivUpdate K (t p) y) + (fun p => revDerivUpdate K (e p) y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + +@[ftrans] +theorem dite.arg_te.revDerivProj_rule + (c : Prop) [dec : Decidable c] + (t : c → X → Y') (e : ¬c → X → Y') + : revDerivProj K (fun x => dite c (t · x) (e · x)) + = + fun y => + dite c (fun p => revDerivProj K (t p) y) + (fun p => revDerivProj K (e p) y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + +@[ftrans] +theorem dite.arg_te.revDerivProjUpdate_rule + (c : Prop) [dec : Decidable c] + (t : c → X → Y') (e : ¬c → X → Y') + : revDerivProjUpdate K (fun x => dite c (t · x) (e · x)) + = + fun y => + dite c (fun p => revDerivProjUpdate K (t p) y) + (fun p => revDerivProjUpdate K (e p) y) := +by + induction dec + case isTrue h => ext y <;> simp[h] + case isFalse h => ext y <;> simp[h] + + +-------------------------------------------------------------------------------- + +section InnerProductSpace + +variable + {R : Type _} [RealScalar R] + -- {K : Type _} [Scalar R K] + {X : Type _} [SemiInnerProductSpace R X] + {Y : Type _} [SemiHilbert R Y] + +-- Inner ----------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +open ComplexConjugate + +@[ftrans] +theorem Inner.inner.arg_a0a1.revDeriv_rule + (f : X → Y) (g : X → Y) + (hf : HasAdjDiff R f) (hg : HasAdjDiff R g) + : (revDeriv R fun x => ⟪f x, g x⟫[R]) + = + fun x => + let y₁df := revDeriv R f x + let y₂dg := revDerivUpdate R g x + (⟪y₁df.1, y₂dg.1⟫[R], + fun dr => + y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1))):= +by + have ⟨_,_⟩ := hf + have ⟨_,_⟩ := hg + simp[revDeriv,revDerivUpdate] + ftrans only; simp + ftrans; simp[smul_pull] + +@[ftrans] +theorem Inner.inner.arg_a0a1.revDerivUpdate_rule + (f : X → Y) (g : X → Y) + (hf : HasAdjDiff R f) (hg : HasAdjDiff R g) + : (revDerivUpdate R fun x => ⟪f x, g x⟫[R]) + = + fun x => + let y₁df := revDerivUpdate R f x + let y₂dg := revDerivUpdate R g x + (⟪y₁df.1, y₂dg.1⟫[R], + fun dr dx => + y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1) dx) ) := + +by + simp[revDerivUpdate] + ftrans; simp[revDerivUpdate,add_assoc] + +@[ftrans] +theorem Inner.inner.arg_a0a1.revDerivProj_rule + (f : X → Y) (g : X → Y) + (hf : HasAdjDiff R f) (hg : HasAdjDiff R g) + : (revDerivProj R fun x => ⟪f x, g x⟫[R]) + = + fun x => + let y₁df := revDeriv R f x + let y₂dg := revDerivUpdate R g x + (⟪y₁df.1, y₂dg.1⟫[R], + fun _ dr => + y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1))) := +by + simp[revDerivProj] + ftrans; simp[StructLike.oneHot, StructLike.make] + +@[ftrans] +theorem Inner.inner.arg_a0a1.revDerivProjUpdate_rule + (f : X → Y) (g : X → Y) + (hf : HasAdjDiff R f) (hg : HasAdjDiff R g) + : (revDerivProjUpdate R fun x => ⟪f x, g x⟫[R]) + = + fun x => + let y₁df := revDerivUpdate R f x + let y₂dg := revDerivUpdate R g x + (⟪y₁df.1, y₂dg.1⟫[R], + fun _ dr dx => + y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1) dx)) := +by + simp[revDerivProjUpdate] + ftrans; simp[revDerivUpdate,add_assoc] + + + +-- norm2 ----------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem SciLean.Norm2.norm2.arg_a0.revDeriv_rule + (f : X → Y) (hf : HasAdjDiff R f) + : (revDeriv R fun x => ‖f x‖₂²[R]) + = + fun x => + let ydf := revDeriv R f x + let ynorm2 := ‖ydf.1‖₂²[R] + (ynorm2, + fun dr => + ((2:R) * dr) • ydf.2 ydf.1):= +by + have ⟨_,_⟩ := hf + funext x; simp[revDeriv] + ftrans only + simp + ftrans + simp[smul_smul] + +@[ftrans] +theorem SciLean.Norm2.norm2.arg_a0.revDerivUpdate_rule + (f : X → Y) (hf : HasAdjDiff R f) + : (revDerivUpdate R fun x => ‖f x‖₂²[R]) + = + fun x => + let ydf := revDerivUpdate R f x + let ynorm2 := ‖ydf.1‖₂²[R] + (ynorm2, + fun dr dx => + ydf.2 (((2:R)*dr)•ydf.1) dx) := +by + have ⟨_,_⟩ := hf + funext x; simp[revDerivUpdate] + ftrans only; simp[revDeriv,smul_pull] + + +@[ftrans] +theorem SciLean.Norm2.norm2.arg_a0.revDerivProj_rule + (f : X → Y) (hf : HasAdjDiff R f) + : (revDerivProj R fun x => ‖f x‖₂²[R]) + = + fun x => + let ydf := revDeriv R f x + let ynorm2 := ‖ydf.1‖₂²[R] + (ynorm2, + fun _ dr => + ((2:R) * dr) • ydf.2 ydf.1):= +by + have ⟨_,_⟩ := hf + funext x; simp[revDerivProj] + ftrans; simp[StructLike.oneHot,StructLike.make] + +@[ftrans] +theorem SciLean.Norm2.norm2.arg_a0.revDerivProjUpdate_rule + (f : X → Y) (hf : HasAdjDiff R f) + : (revDerivProjUpdate R fun x => ‖f x‖₂²[R]) + = + fun x => + let ydf := revDerivUpdate R f x + let ynorm2 := ‖ydf.1‖₂²[R] + (ynorm2, + fun _ dr dx => + ydf.2 (((2:R)*dr)•ydf.1) dx) := +by + have ⟨_,_⟩ := hf + funext x; simp[revDerivProjUpdate] + ftrans only; simp[revDeriv,revDerivUpdate,smul_pull] + + +-- norm₂ ----------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem SciLean.norm₂.arg_x.revDeriv_rule_at + (f : X → Y) (x : X) (hf : HasAdjDiffAt R f x) (hx : f x≠0) + : (revDeriv R (fun x => ‖f x‖₂[R]) x) + = + let ydf := revDeriv R f x + let ynorm := ‖ydf.1‖₂[R] + (ynorm, + fun dr => + (ynorm⁻¹ * dr) • ydf.2 ydf.1):= +by + have ⟨_,_⟩ := hf + simp[revDeriv] + ftrans only + simp + ftrans + funext dr; simp[smul_smul] + +@[ftrans] +theorem SciLean.norm₂.arg_x.revDerivUpdate_rule_at + (f : X → Y) (x : X) (hf : HasAdjDiffAt R f x) (hx : f x≠0) + : (revDerivUpdate R (fun x => ‖f x‖₂[R]) x) + = + let ydf := revDerivUpdate R f x + let ynorm := ‖ydf.1‖₂[R] + (ynorm, + fun dr dx => + ydf.2 ((ynorm⁻¹ * dr)•ydf.1) dx):= +by + have ⟨_,_⟩ := hf + simp[revDerivUpdate] + ftrans only + simp + ftrans + funext dr; simp[revDeriv,smul_pull] + +@[ftrans] +theorem SciLean.norm₂.arg_x.revDerivProj_rule_at + (f : X → Y) (x : X) (hf : HasAdjDiffAt R f x) (hx : f x≠0) + : (revDerivProj R (fun x => ‖f x‖₂[R]) x) + = + let ydf := revDeriv R f x + let ynorm := ‖ydf.1‖₂[R] + (ynorm, + fun _ dr => + (ynorm⁻¹ * dr) • ydf.2 ydf.1):= +by + have ⟨_,_⟩ := hf + simp[revDerivProj] + ftrans only; simp[StructLike.oneHot, StructLike.make] + +@[ftrans] +theorem SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at + (f : X → Y) (x : X) (hf : HasAdjDiffAt R f x) (hx : f x≠0) + : (revDerivProjUpdate R (fun x => ‖f x‖₂[R]) x) + = + let ydf := revDerivUpdate R f x + let ynorm := ‖ydf.1‖₂[R] + (ynorm, + fun _ dr dx => + ydf.2 ((ynorm⁻¹ * dr)•ydf.1) dx):= +by + have ⟨_,_⟩ := hf + simp[revDerivProjUpdate] + ftrans only; simp[revDeriv,revDerivUpdate,smul_pull] + +end InnerProductSpace diff --git a/SciLean/Data/StructLike/Algebra.lean b/SciLean/Data/StructLike/Algebra.lean index 257fae07..5648224e 100644 --- a/SciLean/Data/StructLike/Algebra.lean +++ b/SciLean/Data/StructLike/Algebra.lean @@ -20,33 +20,82 @@ open StructLike in class VecStruct (K X I XI) [StructLike X I XI] [IsROrC K] [Vec K X] [∀ i, Vec K (XI i)] : Prop where proj_add : ∀ i (x x' : X), proj (x + x') i = proj x i + proj x' i proj_smul : ∀ i (k : K) (x : X), proj (k • x) i = k • proj x i - proj_zero : ∀ i, proj (0 : X) i = 0 proj_continuous : Continuous (fun (x : X) i => proj x i) make_continuous : Continuous (fun f => make (X:=X) f) -attribute [simp] VecStruct.proj_add VecStruct.proj_smul VecStruct.proj_zero +attribute [simp, ftrans_simp] VecStruct.proj_add VecStruct.proj_smul -@[neg_pull] -theorem oneHot.arg_xi.neg_pull [StructLike X I XI] [DecidableEq I] [∀ i, Vec K (XI i)] [Vec K X] [VecStruct K X I XI] (i : I) (xi : XI i) - : StructLike.oneHot (X:=X) i (- xi) = - StructLike.oneHot (X:=X) i xi := sorry_proof +-------------------------------------------------------------------------------- +-- VecStruct simps ------------------------------------------------------------- +-------------------------------------------------------------------------------- + +section VecStruct +open StructLike + +variable {X XI} + [StructLike X I XI] [DecidableEq I] [∀ i, Vec K (XI i)] [Vec K X] [VecStruct K X I XI] + +-- TODO prove that `proj`, `make` and `oneHot` are linear functions and generate pull/push theorems +-- probably mark `proj.arg_x.add_pull` and `proj.arg_x.smul_pull` with simp and ftrans_simp attributes +-- probably mark `make.arg_f.add_push` and `make.arg_x.smul_push` with simp and ftrans_simp attributes +-- `make.arg_f.sub_push`, `make.arg_f.neg_push`, ... + + +@[simp,ftrans_simp] +theorem VecStruct.proj_zero (i : I) + : proj (0 : X) i = (0 : XI i) := sorry_proof + +-- the following theorems about oneHot should be automatically generated from linearity of `oneHot` in `xi` @[smul_push] -theorem oneHot.arg_xi.smul_push [StructLike X I XI] [DecidableEq I] [∀ i, Vec K (XI i)] [Vec K X] [VecStruct K X I XI] (i : I) (xi : XI i) (k : K) - : k • StructLike.oneHot (X:=X) i xi = StructLike.oneHot (X:=X) i (k•xi) := sorry_proof +theorem oneHot.arg_xi.smul_push (i : I) (xi : XI i) (k : K) + : k • StructLike.oneHot (X:=X) i xi = StructLike.oneHot (X:=X) i (k•xi) := +by + apply StructLike.ext; intro j + simp[StructLike.oneHot] + if h : i=j then subst h; simp else simp[h] +@[smul_pull] +theorem oneHot.arg_xi.smul_pull (i : I) (xi : XI i) (k : K) + : oneHot (X:=X) i (k•xi) = k • oneHot (X:=X) i xi := +by + apply StructLike.ext; intro j + simp[oneHot] + if h : i=j then subst h; simp else simp[h] + +@[neg_push] +theorem oneHot.arg_xi.neg_push (i : I) (xi : XI i) + : - oneHot (X:=X) i xi = oneHot (X:=X) i (- xi) := +by + apply ext; intro j + have h : ∀ (x : X), -x = (-1:K)•x := by simp + simp [h,smul_push] + +@[neg_pull] +theorem oneHot.arg_xi.neg_pull (i : I) (xi : XI i) + : oneHot (X:=X) i (- xi) = - oneHot (X:=X) i xi := +by + apply ext; intro j + have h : ∀ (x : X), -x = (-1:K)•x := by simp + simp [h,smul_push] @[simp] -theorem oneHot_zero [StructLike X I XI] [DecidableEq I] [∀ i, Vec K (XI i)] [Vec K X] [VecStruct K X I XI] (i : I) - : StructLike.oneHot (X:=X) i 0 = (0 : X) := sorry_proof +theorem oneHot_zero (i : I) + : oneHot (X:=X) i 0 = (0 : X) := sorry_proof @[simp] -theorem add_oneHot_eq_modify [StructLike X I XI] [DecidableEq I] [∀ i, Vec K (XI i)] [Vec K X] [VecStruct K X I XI] (i : I) (xi : XI i) (x : X) - : x + StructLike.oneHot (X:=X) i xi = StructLike.modify i (fun xi' => xi' + xi) x := sorry_proof +theorem add_oneHot_eq_modify (i : I) (xi : XI i) (x : X) + : x + oneHot (X:=X) i xi = modify i (fun xi' => xi' + xi) x := sorry_proof @[simp] -theorem add_oneHot_eq_modify' [StructLike X I XI] [DecidableEq I] [∀ i, Vec K (XI i)] [Vec K X] [VecStruct K X I XI] (i : I) (xi : XI i) (x : X) - : StructLike.oneHot (X:=X) i xi + x = StructLike.modify i (fun xi' => xi + xi') x := sorry_proof +theorem add_oneHot_eq_modify' (i : I) (xi : XI i) (x : X) + : oneHot (X:=X) i xi + x = modify i (fun xi' => xi + xi') x := sorry_proof + +end VecStruct + + +-------------------------------------------------------------------------------- open StructLike in class SemiInnerProductSpaceStruct (K X I XI) [StructLike X I XI] [IsROrC K] [EnumType I] [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)] extends VecStruct K X I XI : Prop where @@ -64,7 +113,6 @@ theorem inner_oneHot_eq_inner_proj' [StructLike X I XI] [EnumType I] [∀ i, Sem instance (priority:=low) {X} [Vec K X] : VecStruct K X Unit (fun _ => X) where proj_add := by simp[StructLike.proj] proj_smul := by simp[StructLike.proj] - proj_zero := by simp[StructLike.proj] proj_continuous := sorry_proof make_continuous := sorry_proof @@ -84,7 +132,6 @@ instance [Vec K E] [Vec K F] [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] : VecStruct K (E×F) (I⊕J) (Prod.TypeFun EI FJ) where proj_add := by simp[StructLike.proj] proj_smul := by simp[StructLike.proj] - proj_zero := by simp[StructLike.proj] proj_continuous := sorry_proof make_continuous := sorry_proof diff --git a/SciLean/Data/StructLike/Basic.lean b/SciLean/Data/StructLike/Basic.lean index 22b551e7..5f4cb6ea 100644 --- a/SciLean/Data/StructLike/Basic.lean +++ b/SciLean/Data/StructLike/Basic.lean @@ -73,7 +73,17 @@ instance (priority:=low+1) left_inv := by simp[LeftInverse] right_inv := by simp[Function.RightInverse, LeftInverse] proj_modify := by simp - proj_modify' := by sorry_proof + proj_modify' := by + intro ⟨i,j⟩ ⟨i',j'⟩; intros _ _ H; simp + if h: i' = i then + subst h + if h': j=j' then + simp[h'] at H + else + simp[proj_modify' _ _ _ _ h'] + else + simp[h] + instance (E I J : Type _) (EI : I → Type _) @@ -89,7 +99,16 @@ instance left_inv := by simp[LeftInverse] right_inv := by simp[Function.RightInverse, LeftInverse] proj_modify := by simp - proj_modify' := by intro (j,i) (j',i') f x _h; simp; sorry_proof + proj_modify' := by + intro (j,i) (j',i') f x H; simp + if h: j = j' then + subst h + if h': i=i' then + simp[h'] at H + else + simp[h'] + else + simp[h] -------------------------------------------------------------------------------- @@ -120,9 +139,5 @@ instance [StructLike E I EI] [StructLike F J FJ] --------------------------------------------------------------------------------- --- TODO: Add some lawfulness w.r.t. to +,•,0 - -