Commit f464b139 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove necessary lemma to get multiplication in structure similar to Coq, start working on proof

parent 87d70593
let REAL_MUL_LE_COMPAT_NEG_L =
prove (`!(a:real) b c.
a <= &0 /\ b <= c ==>
a * c <= a * b`,
intros "!a b c; a_leq_0 b_leq_c"
THEN ONCE_REWRITE_TAC [SYM (SPEC `a:real` REAL_NEG_NEG)]
THEN ONCE_REWRITE_TAC [SYM (SPECL [`a:real`; `c:real`] REAL_MUL_LNEG)]
THEN ONCE_REWRITE_TAC [REAL_LE_NEG]
THEN MATCH_MP_TAC REAL_LE_LMUL
THEN split
THENL [
ONCE_REWRITE_TAC [SYM (SPEC `-- (a:real)` REAL_NEG_LE0)]
THEN ONCE_REWRITE_TAC [REAL_NEG_NEG]
THEN ASM_SIMP_TAC[];
ASM_SIMP_TAC[] ]);;
......@@ -3,6 +3,7 @@
*)
needs "Infra/tactics.hl";;
needs "Infra/Abbrevs.hl";;
needs "Infra/RealSimps.hl";;
needs "Expressions.hl";;
let valid = define
......@@ -203,16 +204,31 @@ g `!(iv1:interval) (iv2:interval) (a:real) (b:real).
e (SIMP_TAC[contained; multInterval; absIntvUpd; IVlo; IVhi]);;
e (intros "!a b; contained_a lo_leq_b b_leq_hi");;
e (destruct "contained_a" "lo_leq_a a_leq_hi");;
e (LABEL_TAC "min4_correct" (SPECL [`(FST I1 * FST I2):real`; `(FST I1 * SND I2):real`; `(SND I1 * FST I2):real`; `(SND I1 * SND I2):real`] min4_correct));;
e (LABEL_TAC "max4_correct" (SPECL [`(FST I1 * FST I2):real`; `(FST I1 * SND I2):real`; `(SND I1 * FST I2):real`; `(SND I1 * SND I2):real`] max4_correct));;
e (LABEL_TAC "min4_correct"
(SPECL
[`FST (I1:real#real) * FST (I2:real#real)`; `FST (I1:real#real) * SND (I2:real#real)`; `SND (I1:real#real) * FST (I2:real#real)`; `SND (I1:real#real) * SND (I2:real#real)`] min4_correct));;
e (LABEL_TAC "max4_correct" (SPECL [`FST (I1:real#real) * FST (I2:real#real)`; `FST (I1:real#real) * SND (I2:real#real)`; `SND (I1:real#real) * FST (I2:real#real)`; `SND (I1:real#real) * SND (I2:real#real)`] max4_correct));;
e (destruct "min4_correct" "leq_lolo leq_lohi leq_hilo leq_hihi");;
e (destruct "max4_correct" "lolo_leq lohi_leq hilo_leq hihi_leq");;
e (split);;
(* Lower Bound *) (* REAL_LE_NEGTOTAL or REAL_LE_NEG??? *)
e (LABEL_TAC "cases_a" (SPECL [`a:real`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_a" "a_lt_0 | 0_leq_a");;
e (LABEL_TAC "cases_hi2" (SPECL [`(SND I2):real`; `&0:real`] REAL_LTE_TOTAL));;
e (LABEL_TAC "cases_hi2" (SPECL [`(SND (I2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2");;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `SND (I1:real#real) * SND (I2:real#real)`);;
e (split);;
e (ASM_SIMP_TAC[]);;
e (ONCE_REWRITE_TAC [REAL_MUL_SYM]);;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `(a:real) * SND (I2:real#real)`);;
e (split);;
(** TODO!!! **)
e (MATCH_MP_TAC (SPECL [`a:real`; `b:real`; `SND (I2:real#real)`] REAL_MUL_LE_COMPAT_NEG_L));;
SPECL [`a:real`; `b:real`; `SND (I2:real#real)`] REAL_MUL_LE_COMPAT_NEG_L;;
REAL_MUL_LE_COMPAT_NEG_L;;
e
(*
TODO FIXME!
e (MATCH_MP_TAC REAL_MULT_LE);;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment