| TacticAst.Reflexivity _ -> Tactics.reflexivity
| TacticAst.Assumption _ -> Tactics.assumption
| TacticAst.Contradiction _ -> Tactics.contradiction
+(*
+ | TacticAst.Discriminate (_,id) -> Tactics.discriminate id
+*)
| TacticAst.Exists _ -> Tactics.exists
| TacticAst.Fourier _ -> Tactics.fourier
+ | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
| TacticAst.Goal (_, n) -> Tactics.set_goal n
| TacticAst.Left _ -> Tactics.left
| TacticAst.Right _ -> Tactics.right
| TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
| TacticAst.Change of 'term * 'term * 'ident option
| TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
| TacticAst.Fold of reduction_kind * 'term
| TacticAst.Injection of 'ident
| TacticAst.Replace_pattern of 'term pattern * 'term
| TacticAst.LApply (_, term, substs) ->
let f (name, term) = Cic.Name name, term in
Tactics.lapply ~substs:(List.map f substs) term
- | _ -> assert false
let eval_tactical status tac =
let apply_tactic tactic =
let status, cic1 = disambiguate_term status what in
let status, cic2 = disambiguate_term status with_what in
status, TacticAst.Change (loc, cic1, cic2, ident)
+ | TacticAst.Generalize (loc,term,pattern) ->
+ let status,term = disambiguate_term status term in
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Generalize(loc,term,pattern)
(*
(* TODO Zack a lot more of tactics to be implemented here ... *)
| TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
let status, term = disambiguate_term status term in
let status, substs = List.fold_left f (status, []) substs in
status, TacticAst.LApply (loc, term, substs)
-
- | x ->
- print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
- assert false
let rec disambiguate_tactical status = function
| TacticAst.Tactic (loc, tactic) ->
--- /dev/null
+inductive nat : Set \def
+ O : nat
+ | S : nat \to nat.
+
+inductive le (n:nat) : nat \to Prop \def
+ leO : le n n
+ | leS : \forall m. le n m \to le n (S m).
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
+theorem test_inversion: \forall n. le n O \to n=O.
+ intros.
+ cut O=O.
+ (* goal 2: 0 = 0 *)
+ goal 7. reflexivity.
+ (* goal 1 *)
+ generalize Hcut. (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
+ apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
+ intro. reflexivity.
+ simplify. intros.
+ (* manca discriminate H3 *)
+qed.
\ No newline at end of file