Not tested yet.
*)
+(******************** OTHER USEFUL TACTICS **********************)
+
+let rewrite_tac ~term:equality ~status:(proof,goal) =
+ let module C = Cic in
+ let module U = UriManager in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let ty,t1,t2 =
+ match CicTypeChecker.type_of_aux' metasenv context equality with
+ C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
+ when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
+ ty,t1,t2
+ | _ ->
+ raise
+ (ProofEngineTypes.Fail
+ "Rewrite: the argument is not a proof of an equality")
+ in
+ let pred =
+ let gty' = CicSubstitution.lift 1 gty in
+ let t1' = CicSubstitution.lift 1 t1 in
+ let gty'' =
+ ProofEngineReduction.replace_lifting
+ ~equality:ProofEngineReduction.syntactic_equality
+ ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+ in
+ C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+ in
+prerr_endline ("##### Atteso: " ^ CicPp.ppterm
+ (C.Lambda (C.Name "x", ty,
+ C.Appl
+ [C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind",0,0) ;
+ ty ; C.Rel 3 ; C.Rel 1]))
+) ;
+prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
+ let eq_ind_r =
+ C.Const
+ (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) in
+ let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let irl =
+ ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+ PrimitiveTactics.exact_tac
+ (C.Appl
+ [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+ ((curi,metasenv',pbo,pty),goal)
+;;
+
+(******************** THE FOURIER TACTIC ***********************)
(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
des inéquations et équations sont entiers. En attendant la tactique Field.
;;
let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
-
+val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
val fourier_tac: ProofEngineTypes.tactic
-
let clear rendering_window =
call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
;;
+let fourier rendering_window =
+ call_tactic ProofEngine.fourier rendering_window
+;;
+let rewrite rendering_window =
+ call_tactic_with_input ProofEngine.rewrite rendering_window
+;;
-let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;;
let whd_in_scratch scratch_window =
let fourierb =
GButton.button ~label:"Fourier"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let rewriteb =
+ GButton.button ~label:"Rewrite"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:"<html><body bgColor=\"white\"></body></html>"
ignore(clearbodyb#connect#clicked (clearbody self)) ;
ignore(clearb#connect#clicked (clear self)) ;
ignore(fourierb#connect#clicked (fourier self)) ;
+ ignore(rewriteb#connect#clicked (rewrite self)) ;
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
-
+let rewrite term = apply_tactic (FourierR.rewrite_tac ~term)
val elim_type : Cic.term -> unit
val ring : unit -> unit
val fourier : unit -> unit
+val rewrite : Cic.term -> unit
aux where
;;
+(* replaces in a term a term with another one. *)
+(* Lifting are performed as usual. *)
+let replace_lifting ~equality ~what ~with_what ~where =
+ let rec substaux k =
+ let module C = Cic in
+ function
+ t when (equality t what) -> CicSubstitution.lift (k-1) with_what
+ | C.Rel n as t -> t (*CSC: ??? BUG ? *)
+ | C.Var _ as t -> t
+ | C.Meta (i, l) as t ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (substaux k t)
+ ) l
+ in
+ C.Meta(i,l')
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.Appl (he::tl) ->
+ (* Invariant: no Appl applied to another Appl *)
+ let tl' = List.map (substaux k) tl in
+ begin
+ match substaux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
+ List.map (substaux k) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+ substaux 1 where
+;;
+
(* Takes a well-typed term and fully reduces it. *)
(*CSC: It does not perform reduction in a Case *)
let reduce context =
val replace :
equality:(Cic.term -> 'a -> bool) ->
what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
+val replace_lifting :
+ equality:(Cic.term -> 'a -> bool) ->
+ what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
val reduce : Cic.context -> Cic.term -> Cic.term
val simpl : Cic.context -> Cic.term -> Cic.term
projects / helm.git / commitdiff