From 6e231a0412e6976c68afacecc775c7f1d0b27380 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Mon, 31 Jul 2023 02:27:12 +0200 Subject: [PATCH] isomorphism axioms for trigonometric functions --- SciLean/FTrans/Isomorph/Basic.lean | 40 +++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/SciLean/FTrans/Isomorph/Basic.lean b/SciLean/FTrans/Isomorph/Basic.lean index 6524218d..0b0407bf 100644 --- a/SciLean/FTrans/Isomorph/Basic.lean +++ b/SciLean/FTrans/Isomorph/Basic.lean @@ -324,6 +324,44 @@ axiom HDiv.hDiv.arg_a0.isomorphFloatToReal (f : α → Float) fun x : α' => (isomorph `FloatToReal f x)⁻¹ +@[ftrans_rule] +axiom Float.exp.arg_a0.isomorphFloatToReal (f : α → Float) + : isomorph `FloatToReal (fun x => Float.exp (f x)) + = + fun x => Real.exp (isomorph `FloatToReal f x) + +@[ftrans_rule] +axiom Float.sin.arg_a0.isomorphFloatToReal (f : α → Float) + : isomorph `FloatToReal (fun x => Float.sin (f x)) + = + fun x => Real.sin (isomorph `FloatToReal f x) + +@[ftrans_rule] +axiom Float.cos.arg_a0.isomorphFloatToReal (f : α → Float) + : isomorph `FloatToReal (fun x => Float.cos (f x)) + = + fun x => Real.cos (isomorph `FloatToReal f x) + +@[ftrans_rule] +axiom Float.asin.arg_a0.isomorphFloatToReal (f : α → Float) + : isomorph `FloatToReal (fun x => Float.asin (f x)) + = + fun x => Real.arcsin (isomorph `FloatToReal f x) + +@[ftrans_rule] +axiom Float.acos.arg_a0.isomorphFloatToReal (f : α → Float) + : isomorph `FloatToReal (fun x => Float.acos (f x)) + = + fun x => Real.arccos (isomorph `FloatToReal f x) + +@[ftrans_rule] +axiom Float.atan.arg_a0.isomorphFloatToReal (f : α → Float) + : isomorph `FloatToReal (fun x => Float.atan (f x)) + = + fun x => Real.arctan (isomorph `FloatToReal f x) + + + @[simp] axiom Zero.zero.isomorphFloatToReal : floatToReal (0 : Float) @@ -342,7 +380,7 @@ instance : Semigroup Float where mul_assoc := by intro a b c apply (isoext `FloatToReal _ _).2 - simp; ftrans; ftrans + ftrans; ftrans; ftrans rw[mul_assoc]