From 27ebdab06ba308c431669b58a46fc0bb12c8c72e Mon Sep 17 00:00:00 2001 From: maiorino Date: Thu, 27 Jul 2006 16:21:27 +0000 Subject: [PATCH] "that is equivalent to" and "or equivalently" implemented in most situations. --- components/grafite_parser/grafiteParser.ml | 2 +- components/tactics/declarative.ml | 54 +++++++++++++++------- matita/matita.lang | 4 ++ matita/tests/decl.ma | 21 +++++---- 4 files changed, 53 insertions(+), 28 deletions(-) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 1eb2a495d..5f256a1e0 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -240,7 +240,7 @@ EXTEND (* Produzioni Aggiunte *) | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> GrafiteAst.Assume (loc, id, t) - | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']-> + | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']-> GrafiteAst.Suppose (loc, t, id, t1) | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc]; cont=by_continuation -> diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 50d4be884..370e326db 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -34,27 +34,34 @@ let assume id t = ;; 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 = @@ -65,12 +72,20 @@ 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' = @@ -197,8 +212,13 @@ let case id ~params = ;; let thesisbecomes t = - (*BUG here: nothing done*) - Tacticals.id_tac +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;; diff --git a/matita/matita.lang b/matita/matita.lang index 3aa42083e..b7198579c 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -131,6 +131,10 @@ assume suppose by + is + or + equivalent + equivalently we prove proved diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma index 8ff56dde8..4359b4a9d 100644 --- a/matita/tests/decl.ma +++ b/matita/tests/decl.ma @@ -130,9 +130,8 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty. we proceed by induction on t to prove False. case Empty. the thesis becomes (O < size Empty → Empty ≠ Empty). - suppose (O < size Empty) (absurd). - (*Bug here: missing that is equivalent to *) - simplify in absurd. + suppose (O < size Empty) (absurd) + that is equivalent to (O < O). (* Here the "natural" language is not natural at all *) we proceed by induction on (trivial absurd) to prove False. (*Bug here: this is what we want @@ -145,11 +144,13 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty. by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1). assume t2: tree. by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2). - suppose (O < size (Node t1 t2)) (Hyp). - (*BUG: that is equivalent to missed here *) - unfold Not. - suppose (Node t1 t2 = Empty) (absurd). - (* Discriminate should really generate a theorem to be useful with - declarative tactics *) - discriminate absurd. + suppose (O < size (Node t1 t2)) (useless). + we need to prove (Node t1 t2 ≠ Empty) (final) + or equivalently (Node t1 t2 = Empty → False). + suppose (Node t1 t2 = Empty) (absurd). + (* Discriminate should really generate a theorem to be useful with + declarative tactics *) + discriminate absurd. + by final + done. qed. \ No newline at end of file -- 2.39.2