components/tactics/declarative.ml

   1 let assume id t =
   2  Tacticals.then_
   3   ~start:
   4     (Tactics.intros ~howmany:1
   5       ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
   6   ~continuation:
   7     (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
   8      (fun _ metasenv ugraph -> t,metasenv,ugraph))
   9 ;;
  10
  11 let suppose t id =
  12  Tacticals.then_
  13    ~start:
  14        (Tactics.intros ~howmany:1
  15              ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  16    ~continuation:
  17             (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  18               (fun _ metasenv ugraph -> t,metasenv,ugraph))
  19 ;;
  20
  21 let by_term_we_proved t ty id =
  22  Tacticals.thens
  23  ~start:
  24    (Tactics.cut ty
  25      ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  26  ~continuations:
  27    [ Tacticals.id_tac ; Tactics.apply t ]
  28 ;;
  29
  30 let bydone t =
  31    (Tactics.apply ~term:t)
  32
  33 ;;
  34
  35 let we_need_to_prove t id =
  36  let aux status =
  37   let proof,goals =
  38    ProofEngineTypes.apply_tactic
  39     (Tactics.cut t
  40       ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  41     status
  42   in
  43    let goals' =
  44     match goals with
  45        [fst; snd] -> [snd; fst]
  46      | _ -> assert false
  47    in
  48     proof,goals'
  49  in
  50   ProofEngineTypes.mk_tactic aux
  51 ;;