How to use a Coq lambda term?
It is not so obvious how a Coq lambda term can be used in Coq. Adding the same Require statements included in the non lambda version of the Coq proof and just adding a Definition test := in front of the term leads to an error about holes. It is not clear to me if this is caused by missing Require statements (maybe some type class instances) or if the term possibly needs a type annotation to fix the holes.
Example gappa script:
Rexact = 2*x;
Rapprox float<ieee_32,ne>= 2*x;
{
@FLT(x,24) /\ x in [0, 1] ->
|Rapprox - Rexact| <= 1e-7
}
Example augmented generated Coq lambda script:
Require Import Gappa.Gappa_library.
Definition test :=
(fun (_x : Reals.Rdefinitions.R) =>
let p1 := Gappa.Gappa_definitions.FLT _x (24) in (* FLT(x, 24) *)
let f1 := Gappa.Gappa_definitions.Float2 (0) (0) in
let f2 := Gappa.Gappa_definitions.Float2 (1) (0) in
let i1 := Gappa.Gappa_definitions.makepairF f1 f2 in
let p2 := Gappa.Gappa_definitions.BND _x i1 in (* BND(x, [0, 1]) *)
let s2 := p1 /\ p2 in
let r6 := Gappa.Gappa_pred_bnd.Float1 (2) in
let _Rexact := Reals.Rdefinitions.Rmult r6 _x in
let _Rapprox := (Gappa.Gappa_float.rounding_float Gappa.Gappa_round_def.rndNE (24)%positive (-149)%Z) _Rexact in
let r3 := Reals.Rdefinitions.Rminus _Rapprox _Rexact in
let r2 := Reals.Rbasic_fun.Rabs r3 in
let f3 := Gappa.Gappa_definitions.Float2 (967140655691703339) (-83) in
let i2 := Gappa.Gappa_definitions.makepairF f1 f3 in
let p3 := Gappa.Gappa_definitions.BND r2 i2 in (* BND(|Rapprox - Rexact|, [0, 1e-07]) *)
let s3 := not p3 in
let s1 := s2 /\ s3 in
let l2 : s1 -> s3 :=
fun h0 =>
let h1 := h0 in
proj2 h1 in
let f4 := Gappa.Gappa_definitions.Float2 (1) (-24) in
let i3 := Gappa.Gappa_definitions.makepairF f1 f4 in
let p4 := Gappa.Gappa_definitions.BND r2 i3 in (* BND(|Rapprox - Rexact|, [0, 5.96046e-08]) *)
let p5 := Gappa.Gappa_definitions.ABS r3 i3 in (* ABS(Rapprox - Rexact, [0, 5.96046e-08]) *)
let f5 := Gappa.Gappa_definitions.Float2 (-1) (-24) in
let i4 := Gappa.Gappa_definitions.makepairF f5 f4 in
let p6 := Gappa.Gappa_definitions.BND r3 i4 in (* BND(Rapprox - Rexact, [-5.96046e-08, 5.96046e-08]) *)
let f6 := Gappa.Gappa_definitions.Float2 (1) (1) in
let i5 := Gappa.Gappa_definitions.makepairF f1 f6 in
let p7 := Gappa.Gappa_definitions.ABS _Rexact i5 in (* ABS(Rexact, [0, 2]) *)
let p8 := Gappa.Gappa_definitions.BND _Rexact i5 in (* BND(Rexact, [0, 2]) *)
let i6 := Gappa.Gappa_definitions.makepairF f2 f6 in
let p9 := Gappa.Gappa_definitions.BND r6 i6 in (* BND(2, [1, 2]) *)
let t1 : p9 := Gappa.Gappa_pred_bnd.constant1 _ i6 _ in
let l8 : s1 -> p9 (* BND(2, [1, 2]) *) :=
fun h0 =>
t1 in
let l10 : s1 -> s2 :=
fun h0 =>
let h1 := h0 in
proj1 h1 in
let l9 : s1 -> p2 (* BND(x, [0, 1]) *) :=
fun h0 =>
let h1 := l10 h0 in
proj2 h1 in
let t2 (h0 : p9) (h1 : p2) : p8 := Gappa.Gappa_pred_bnd.mul_pp r6 _x i6 i1 i5 h0 h1 _ in
let l7 : s1 -> p8 (* BND(Rexact, [0, 2]) *) :=
fun h0 =>
let h1 := l8 h0 in
let h2 := l9 h0 in
t2 h1 h2 in
let t3 (h0 : p8) : p7 := Gappa.Gappa_pred_abs.abs_of_bnd_p _Rexact i5 i5 h0 _ in
let l6 : s1 -> p7 (* ABS(Rexact, [0, 2]) *) :=
fun h0 =>
let h1 := l7 h0 in
t3 h1 in
let t4 (h0 : p7) : p6 := Gappa.Gappa_float.float_absolute_wide_ne _ _ _Rexact i5 i4 h0 _ in
let l5 : s1 -> p6 (* BND(Rapprox - Rexact, [-5.96046e-08, 5.96046e-08]) *) :=
fun h0 =>
let h1 := l6 h0 in
t4 h1 in
let t5 (h0 : p6) : p5 := Gappa.Gappa_pred_abs.abs_of_bnd_o r3 i4 i3 h0 _ in
let l4 : s1 -> p5 (* ABS(Rapprox - Rexact, [0, 5.96046e-08]) *) :=
fun h0 =>
let h1 := l5 h0 in
t5 h1 in
let t6 (h0 : p5) : p4 := Gappa.Gappa_pred_abs.uabs_of_abs r3 i3 h0 in
let l3 : s1 -> p4 (* BND(|Rapprox - Rexact|, [0, 5.96046e-08]) *) :=
fun h0 =>
let h1 := l4 h0 in
t6 h1 in
let l1 : s1 -> False :=
fun h0 =>
let h1 := l2 h0 in
let h2 := l3 h0 in
simplify (Tatom false (Abnd 0%nat i2)) Tfalse (Abnd 0%nat i3) (List.cons r2 List.nil) h2 h1 _ in
l1)
.
This leads to error:
Cannot infer this placeholder of type
"constant2_helper {| Fnum := 2; Fexp := 0 |} i6 = true" in environment:
_x : R
for the hole in
let t1 : p9 := Gappa.Gappa_pred_bnd.constant1 _ i6 _ in