des inéquations et équations sont entiers. En attendant la tactique Field.
*)
-(*open Term // in coq/kernel
-open Tactics
-open Clenv
-open Names
-open Tacmach*)
open Fourier
(******************************************************************************
i.e. on obtient une contradiction.
*)
+let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
+let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
+let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
+let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
+let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
+let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
+let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
+let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
+let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
+let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
+let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
+let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
+let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
+let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
+let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
+let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
+let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
+let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
+let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
+let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
+let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
+
+let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
+
+let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
+
+let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
+
+
let is_int x = (x.den)=1
;;
(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
*)
-(*et int_to_real n =
- let nn=abs n in
- let s=ref Cic.term
- if nn=0
- then s:="R0"
- else (s:="R1";
- for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
- if n<0 then s:="(Ropp "^(!s)^")";
- !s
-;;*)
-let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
-
-let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
-let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
-let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-
let rec int_to_real_aux n =
match n with
(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
*)
-let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
-let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
-
let rational_to_real x =
let (n,d)=rational_to_fraction x in
(* preuve que 0<n*1/d
*)
-let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
-
-let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
-
-let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
-
-
let tac_zero_inf_pos gl (n,d) =
(*let cste = pf_parse_constr gl in*)
let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
(* preuve que 0<=n*1/d
*)
-(*let tac_zero_infeq_pos gl (n,d)=
- let cste = pf_parse_constr gl in
- let tacn=ref (if n=0
- then (apply (cste "Rle_zero_zero"))
- else (apply (cste "Rle_zero_1"))) in
- let tacd=ref (apply (cste "Rlt_zero_1")) in
+
+let tac_zero_infeq_pos gl (n,d) =
+ (*let cste = pf_parse_constr gl in*)
+ let tacn = ref (if n=0 then
+ (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
+ else
+ (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
+ in
+ let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
for i=1 to n-1 do
- tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
+ tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
for i=1 to d-1 do
- tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
- (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
-;;*)
-
+ tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
+;;
+
+
+
(* preuve que 0<(-n)*(1/d) => False
*)
-(*let tac_zero_inf_false gl (n,d) =
- let cste = pf_parse_constr gl in
- if n=0 then (apply (cste "Rnot_lt0"))
+
+let tac_zero_inf_false gl (n,d) =
+ if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
else
- (tclTHEN (apply (cste "Rle_not_lt"))
- (tac_zero_infeq_pos gl (-n,d)))
-;;*)
+ (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
+ ~continuation:(tac_zero_infeq_pos gl (-n,d)))
+;;
(* preuve que 0<=(-n)*(1/d) => False
*)
-(*let tac_zero_infeq_false gl (n,d) =
- let cste = pf_parse_constr gl in
- (tclTHEN (apply (cste "Rlt_not_le"))
- (tac_zero_inf_pos gl (-n,d)))
+
+let tac_zero_infeq_false gl (n,d) =
+ (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+ ~continuation:(tac_zero_inf_pos gl (-n,d)))
;;
+
+(* *********** ********** ******** ??????????????? *********** **************
+
+let mkMeta proof = Cic.Meta (ProofEngineHelpers.new_meta proof) (ProofEngineHelpers.identity_relocation_list_for_metavariable []);;
+
+let apply_type_tac t al (proof,goals) =
+ let new_m = mkMeta proof in
+ PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast new_m t)::al))
+;;
+
+
+
+
let create_meta () = mkMeta(new_meta());;
let my_cut c gl=
let concl = pf_concl gl in
apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
;;
-let exact = exact_check;;
+
+*********** * ********************************* ***************************** *)
+
+let exact = PrimitiveTactics.exact_tac;;
let tac_use h = match h.htype with
- "Rlt" -> exact h.hname
- |"Rle" -> exact h.hname
- |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
- (exact h.hname))
- |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
- (exact h.hname))
- |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
- (exact h.hname))
- |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
- (exact h.hname))
+ "Rlt" -> exact ~term:h.hname
+ |"Rle" -> exact ~term:h.hname
+ |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
+ ~continuation:(exact ~term:h.hname))
+ |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
+ ~continuation:(exact ~term:h.hname))
+ |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
+ ~continuation:(exact ~term:h.hname))
+ |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
+ ~continuation:(exact ~term:h.hname))
|_->assert false
;;
+
+
+(* servono tutti ????????????????????????? *)
+let uri_of_term t =
+ match t with
+ Cic.Const(u,_) -> u
+ |Cic.Var(u) -> u
+ |Cic.MutInd(u,_,_) -> u
+ |Cic.MutConstruct(u,_,_,_) -> u
+ |Cic.MutCase(u,_,_,_,_,_) -> u
+ | _ -> UriManager.uri_of_string "??????"
+ ;;
+
+
+
let is_ineq (h,t) =
- match (kind_of_term t) with
- App (f,args) ->
- (match (string_of_constr f) with
- "Coq.Reals.Rdefinitions.Rlt" -> true
- |"Coq.Reals.Rdefinitions.Rgt" -> true
- |"Coq.Reals.Rdefinitions.Rle" -> true
- |"Coq.Reals.Rdefinitions.Rge" -> true
- |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
- "Coq.Reals.Rdefinitions.R"->true
+ match t with
+ Cic.Appl ( Cic.Const(u,boh)::next) ->
+ (match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
+ |"cic:/Coq/Init/Logic_Type/eqT.con" -> (match (UriManager.string_of_uri (uri_of_term(List.hd next))) with
+ "cic:/Coq/Reals/Rdefinitions/R.con"->true
|_->false)
|_->false)
|_->false
let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
let mkAppL a =
- let l = Array.to_list a in
- mkApp(List.hd l, Array.of_list (List.tl l))
-;;*)
+ Cic.Appl(Array.to_list a)
+;;
(* Résolution d'inéquations linéaires dans R *)
-
-(*
-let rec fourier gl=
- let parse = pf_parse_constr gl in
- let goal = strip_outer_cast (pf_concl gl) in
- let fhyp=id_of_string "new_hyp_for_fourier" in
+let rec strip_outer_cast c = match c with
+ | Cic.Cast (c,_) -> strip_outer_cast c
+ | _ -> c
+
+(* se pf_concl estrae la concl*)
+(*let rec fourier ~status:(((p_uri,p_meta,p_incom,p_tes) as proof,goal) as status)=
+ let goal = strip_outer_cast p_tes in
+ let fhyp = String.copy "new_hyp_for_fourier" in *)
(* si le but est une inéquation, on introduit son contraire,
et le but à prouver devient False *)
- try (let tac =
- match (kind_of_term goal) with
- App (f,args) ->
- (match (string_of_constr f) with
- "Coq.Reals.Rdefinitions.Rlt" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rle" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_gt_le"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rgt" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_le_gt"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rge" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
- (intro_using fhyp))
- fourier)
+(* try (let tac =
+ match goal with
+ Cic.Appl ( Cic.Const(u,boh)::args) ->
+ (match UriManager.string_of_uri u with
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
+ (Tacticals.then_
+ ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
+ ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
+ ~continuation:fourier)
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
+ (Tacticals.then_
+ ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
+ ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
+ ~continuation:fourier)
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
+ (Tacticals.then_
+ ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
+ ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
+ ~continuation:fourier)
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
+ (Tacticals.then_
+ ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
+ ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
+ ~continuation:fourier)
|_->assert false)
|_->assert false
- in tac gl)
- with _ ->
-*)
+ in tac status)
+ with _ -> *)
+
(* les hypothèses *)
-(*
- let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
+ (***** Come estraggo pf_hyps?????????????? *******)
+(* let hyps = List.map (fun (h,t) -> (Cic.Var(h),t))
(list_of_sign (pf_hyps gl)) in
let lineq =ref [] in
List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
with _-> ())
hyps;
-*)
-
+
+ *)
(* lineq = les inéquations découlant des hypothèses *)
projects / helm.git / commitdiff