| GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
| GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
| GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
- Declarative.by_term_we_proved t ty id t1
+ Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) t ty id t1
| GrafiteAst.We_need_to_prove (_, t, id, t2) ->
Declarative.we_need_to_prove t id t2
- | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
+ | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) t
| GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
Declarative.we_proceed_by_induction_on t t1
- | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction id t
+ | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
| GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
| GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
Declarative.existselim t id1 t1 id2 t2
| GrafiteAst.Case (_,id,params) -> Declarative.case id params
| GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
| GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
- Declarative.rewritingstep termine t1 t2 cont
+ Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) termine t1 t2 cont
let classify_tactic tactic =
match tactic with
(fun _ metasenv ugraph -> ty,metasenv,ugraph))
;;
-let by_term_we_proved t ty id ty' =
- match t with
- None -> assert false
- | Some 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 by_term_we_proved ~dbd t ty id ty' =
+ let just =
+ match t with
+ None -> Tactics.auto ~dbd ~params:[]
+ | Some t -> Tactics.apply t
+ in
+ 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 ; just ]
;;
-let bydone t =
- match t with
- None -> assert false
- | Some t ->
- (Tactics.apply ~term:t)
+let bydone ~dbd t =
+ let just =
+ match t with
+ None -> Tactics.auto ~dbd ~params:[]
+ | Some t -> Tactics.apply t
+ in
+ just
;;
let we_need_to_prove t id ty =
let andelim = existselim;;
-let rewritingstep lhs rhs just conclude =
+let rewritingstep ~dbd lhs rhs just conclude =
let aux ((proof,goal) as status) =
let (curi,metasenv,proofbo,proofty) = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let eq,trans =
match LibraryObjects.eq_URI () with
- None -> assert false (*TODO*)
+ None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
| Some uri ->
Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
in
CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
let just =
match just with
- None -> assert false (*TOOD*)
- | Some just -> just
+ None ->
+ Tactics.auto ~dbd
+ ~params:["paramodulation","on"; "timeout","3"]
+ | Some just -> Tactics.apply just
in
match lhs with
None ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- Tactics.apply just]) status
+ just]) status
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- Tactics.apply just]
+ just]
]) status)
| Some lhs ->
match conclude with
- None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
+ None -> ProofEngineTypes.apply_tactic just status
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
~start:
(Tactics.cut ~mk_fresh_name_callback
(Cic.Appl [eq ; ty ; lhs ; rhs]))
- ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
+ ~continuations:[ Tacticals.id_tac ; just ]) status
in
ProofEngineTypes.mk_tactic aux
;;
val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
-val by_term_we_proved : Cic.term option -> Cic.term -> string -> Cic.term option ->ProofEngineTypes.tactic
+val by_term_we_proved :
+ dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string -> Cic.term option ->
+ ProofEngineTypes.tactic
-val bydone : Cic.term option -> ProofEngineTypes.tactic
+val bydone : dbd:HMysql.dbd -> Cic.term option -> ProofEngineTypes.tactic
val we_need_to_prove :
Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
val rewritingstep :
- Cic.term option -> Cic.term -> Cic.term option -> Cic.name option ->
- ProofEngineTypes.tactic
+ dbd:HMysql.dbd -> Cic.term option -> Cic.term -> Cic.term option ->
+ Cic.name option -> ProofEngineTypes.tactic
]
qed.
+theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
+ assume n: nat.
+ assume m: nat.
+ (* base case *)
+ by _ we proved (O = O) (trivial).
+ by _ we proved (O = O ∨ m = O) (trivial2).
+ by _ we proved (O*m=O → O=O ∨ m=O) (base_case).
+ (* inductive case *)
+ we need to prove
+ (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
+ (inductive_case).
+ assume n1: nat.
+ suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
+ (* base case *)
+ by _ we proved (S n1 = O ∨ O = O) (pre_base_case2).
+ by _ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+ (* inductive case *)
+ we need to prove
+ (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
+ (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
+ assume m1: nat.
+ suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
+ suppose (S n1 * S m1 = O) (absurd_hyp).
+ simplify in absurd_hyp.
+ by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+ (* BUG: automation failure *)
+ by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+ (* BUG: automation failure *)
+ by (False_ind ? the_absurd)
+ done.
+ (* the induction *)
+ by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ done.
+ (* the induction *)
+ by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+done.
+qed.
theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
assume P: Prop.
done.
qed.
+theorem easy45: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
+assume n: nat.
+assume m:nat.
+assume p:nat.
+suppose (n=m) (H).
+suppose (S m = S p) (K).
+suppose (n = S p) (L).
+obtain (S n) = (S m) by _.
+ = (S p) by _.
+ = n by _
+done.
+qed.
+
theorem easy5: ∀n:nat. n*O=O.
assume n: nat.
(* Bug here: False should be n*0=0 *)
projects / helm.git / commitdiff