;;
let suppose t id ty =
-(*BUG: ty not used *)
+(*BUG: check on t missing *)
+ let ty = match ty with None -> t | Some ty -> ty in
Tacticals.then_
~start:
- (Tactics.intros ~howmany:1
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+ (Tactics.intros ~howmany:1
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
~continuation:
- (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
- (fun _ metasenv ugraph -> t,metasenv,ugraph))
+ (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph))
;;
let by_term_we_proved t ty id ty' =
-(*BUG: ty' not used *)
match t with
None -> assert false
| Some t ->
- Tacticals.thens
- ~start:
- (Tactics.cut ty
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
- ~continuations:
- [ Tacticals.id_tac ; Tactics.apply t ]
+ let continuation =
+ match ty' with
+ None -> Tacticals.id_tac
+ | Some ty' ->
+ Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph)
+ in
+ Tacticals.thens
+ ~start:
+ (Tactics.cut ty
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ ~continuations:
+ [ continuation ; Tactics.apply t ]
;;
let bydone t =
;;
let we_need_to_prove t id ty =
-(*BUG: ty not used *)
let aux status =
+ let cont,cutted =
+ match ty with
+ None -> Tacticals.id_tac,t
+ | Some ty ->
+ Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
let proof,goals =
ProofEngineTypes.apply_tactic
- (Tactics.cut t
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ (Tacticals.thens
+ ~start:
+ (Tactics.cut cutted
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ ~continuations:[cont])
status
in
let goals' =
ProofEngineTypes.mk_tactic aux
;;
-let case _ = assert false
-;;
-let thesisbecomes _ = assert false
+let we_proceed_by_induction_on t pat =
+ (*BUG here: pat unused *)
+ Tactics.elim_intros ~depth:0 t
;;
-let byinduction _ = assert false
+
+let case id ~params =
+ (*BUG here: id unused*)
+ (*BUG here: it does not verify that the previous branch is closed *)
+ (*BUG here: the params should be parsed telescopically*)
+ (*BUG here: the tactic_terms should be terms*)
+ let rec aux ~params ((proof,goal) as status) =
+ match params with
+ [] -> proof,[goal]
+ | (id,t)::tl ->
+ match ProofEngineTypes.apply_tactic (assume id t) status with
+ proof,[goal] -> aux tl (proof,goal)
+ | _ -> assert false
+ in
+ ProofEngineTypes.mk_tactic (aux ~params)
;;
-let we_proceed_by_induction_on _ = assert false
+
+let thesisbecomes t =
+let ty = None in
+ (*BUG here: missing check on t *)
+ match ty with
+ None -> Tacticals.id_tac
+ | Some ty ->
+ Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph)
;;
+
+let byinduction t id = suppose t id None;;