"that is equivalent to" and "or equivalently" implemented in most situations.

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 1eb2a495d4624bed0709830af6386c4a25e5ec10..5f256a1e06864d2e022a126592e7848b324ab843 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 50d4be88435e650976eda3fd9052f697bd87e0f1..370e326dbcd2f76fcda3efe06593f46e2ef0944c 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/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/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index 3aa42083e6496994b79a22043ce39676bcb2b405..b7198579c4eac2c5b67401d1a2f09a295f6cfcab 100644 (file)
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -131,6 +131,10 @@
     <keyword>assume</keyword>
     <keyword>suppose</keyword>
     <keyword>by</keyword>
+    <keyword>is</keyword>
+    <keyword>or</keyword>
+    <keyword>equivalent</keyword>
+    <keyword>equivalently</keyword>
     <keyword>we</keyword> 
     <keyword>prove</keyword>
     <keyword>proved</keyword>

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index 8ff56dde87398e467896aee5d7c3d58b8266e829..4359b4a9dc4dc9009943a8c3fe10eac142d94129 100644 (file)
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/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