First experimental version of the declarative proof language for Matita.

Supported commands so far:
  assume id: term
  suppose term (id)
  by term done
  by term we proved term (id)
  we need to prove term (id)

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 5896e116fa6f17de2ff832c77c297578105e97bd..73ae34584d282e549736ee7e6231d83f2bec1748 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -85,6 +85,12 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Split of loc
   | Symmetry of loc
   | Transitivity of loc * 'term
+  (* Costruttori Aggiunti *)
+  | Assume of loc * 'ident * 'term
+  | Suppose of loc * 'term *'ident
+  | By_term_we_proved of loc * 'term * 'term * 'ident
+  | We_need_to_prove of loc * 'term * 'ident
+  | Bydone of loc * 'term
 
 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 941f75d9d6dae352574be19861ddc79d1775f2c5..b95df8d366d3a3daf5d70a8efeaac7a20c4875e7 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -154,8 +154,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+  
+  let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index ebe7df36977901b7b8351f3af62db67f45a30306..ab43c6cc18e67c0684562e4ed2a6dffeacb589bf 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -154,6 +154,13 @@ let tactic_of_ast ast =
   | GrafiteAst.Split _ -> Tactics.split
   | GrafiteAst.Symmetry _ -> Tactics.symmetry
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
+  (* Implementazioni Aggiunte *)
+  | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
+  | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
+  | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
+     Declarative.by_term_we_proved t ty id
+  | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
+  | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
 
 (* maybe we only need special cases for apply and goal *)
 let classify_tactic tactic = 

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 6b7dd076bd68840453717b08e627405e7660cae6..b02d57e672ea602f704b21405f652c0eea8e5a58 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -251,6 +251,23 @@ let disambiguate_tactic
     | GrafiteAst.Transitivity (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Transitivity (loc, cic)
+      (* Nuovi casi *)
+    | GrafiteAst.Assume (loc, id, term) -> 
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Assume (loc, id, cic)
+    | GrafiteAst.Suppose (loc, term, id) ->
+        let metasenv,cic = disambiguate_term context metasenv term in 
+       metasenv,GrafiteAst.Suppose (loc, cic, id)
+    | GrafiteAst.Bydone (loc,term) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.Bydone (loc, cic)
+    | GrafiteAst.We_need_to_prove (loc,term,id) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.We_need_to_prove (loc,cic,id)
+    | GrafiteAst.By_term_we_proved (loc,term,term',id) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+        let metasenv,cic' = disambiguate_term context metasenv term' in
+       metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id)
 
 let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
   let uri =

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 1a11ec62f0d788e06a15c55d3c3f3453ccb73e7d..1c85b567d48feb17d98064632c60718f4531f15d 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -231,6 +231,17 @@ EXTEND
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
         GrafiteAst.Transitivity (loc, t)
+     (* Produzioni Aggiunte *)
+    | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+        GrafiteAst.Assume (loc, id, t)
+    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.Suppose (loc, t, id)
+    | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.By_term_we_proved (loc, t, ty, id)
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.We_need_to_prove (loc, t, id)
+    | IDENT "by" ; t = tactic_term ; IDENT "done" ->
+        GrafiteAst.Bydone (loc, t)
     ]
   ];
   atomic_tactical:

diff --git a/components/tactics/.depend b/components/tactics/.depend
index 50083802753f2ac184c1e13d11d1a24ff04aa729..43ed94aa9dd287dcc9f31eed229e25d8ff636aed 100644 (file)
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -24,10 +24,12 @@ autoTactic.cmi: proofEngineTypes.cmi
 discriminationTactics.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 ring.cmi: proofEngineTypes.cmi 
+setoids.cmi: proofEngineTypes.cmi 
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
 tactics.cmi: proofEngineTypes.cmi 
+declarative.cmi: proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
@@ -63,17 +65,19 @@ paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi
 paramodulation/subst.cmo: paramodulation/subst.cmi 
 paramodulation/subst.cmx: paramodulation/subst.cmi 
 paramodulation/equality.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi proofEngineReduction.cmi \
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
     paramodulation/equality.cmi 
 paramodulation/equality.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx proofEngineReduction.cmx \
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
     paramodulation/equality.cmi 
 paramodulation/inference.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi proofEngineHelpers.cmi metadataQuery.cmi \
-    paramodulation/equality.cmi paramodulation/inference.cmi 
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
+    metadataQuery.cmi paramodulation/equality.cmi \
+    paramodulation/inference.cmi 
 paramodulation/inference.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx proofEngineHelpers.cmx metadataQuery.cmx \
-    paramodulation/equality.cmx paramodulation/inference.cmi 
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
+    metadataQuery.cmx paramodulation/equality.cmx \
+    paramodulation/inference.cmi 
 paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
     paramodulation/equality.cmi paramodulation/equality_indexing.cmi 
 paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
@@ -186,3 +190,5 @@ tactics.cmx: variousTactics.cmx tacticals.cmx paramodulation/saturation.cmx \
     introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
     autoTactic.cmx tactics.cmi 
+declarative.cmo: tactics.cmi tacticals.cmi declarative.cmi 
+declarative.cmx: tactics.cmx tacticals.cmx declarative.cmi 

diff --git a/components/tactics/Makefile b/components/tactics/Makefile
index e75a8f3ab331a71d376aa9d54e81a5dc99aead8f..aa16069976a5c9461407fc0007382b08c21a1dd5 100644 (file)
--- a/components/tactics/Makefile
+++ b/components/tactics/Makefile
@@ -18,7 +18,7 @@ INTERFACE_FILES = \
        equalityTactics.mli autoTactic.mli discriminationTactics.mli \
         inversion.mli inversion_principle.mli ring.mli setoids.mli \
        fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \
-       statefulProofEngine.mli tactics.mli
+       statefulProofEngine.mli tactics.mli declarative.mli
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
new file mode 100644 (file)
index 0000000..c22d51a
--- /dev/null
+++ b/components/tactics/declarative.ml
@@ -0,0 +1,51 @@
+let assume id t =
+ Tacticals.then_
+  ~start:
+    (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))
+;;
+
+let suppose t id =
+ Tacticals.then_
+   ~start:
+       (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))
+;;
+
+let by_term_we_proved t ty id =
+ Tacticals.thens
+ ~start:
+   (Tactics.cut ty
+     ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+ ~continuations:
+   [ Tacticals.id_tac ; Tactics.apply t ]
+;;
+
+let bydone t =
+   (Tactics.apply ~term:t)
+
+;;
+
+let we_need_to_prove t id =
+ let aux status =
+  let proof,goals =
+   ProofEngineTypes.apply_tactic
+    (Tactics.cut t
+      ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+    status
+  in
+   let goals' =
+    match goals with
+       [fst; snd] -> [snd; fst]
+     | _ -> assert false
+   in
+    proof,goals'
+ in
+  ProofEngineTypes.mk_tactic aux
+;;

diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli
new file mode 100644 (file)
index 0000000..b745ef5
--- /dev/null
+++ b/components/tactics/declarative.mli
@@ -0,0 +1,5 @@
+val assume : string -> Cic.term -> ProofEngineTypes.tactic
+val suppose : Cic.term -> string -> ProofEngineTypes.tactic
+val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic
+val bydone : Cic.term -> ProofEngineTypes.tactic
+val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic

diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma
new file mode 100644 (file)
index 0000000..285d07c
--- /dev/null
+++ b/matita/tests/decl.ma
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/test/decl".
+
+include "nat/times.ma".
+include "nat/orders.ma".
+
+theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
+ assume n: nat.
+ assume m: nat.
+ (* base case *)
+ by (refl_eq ? O) we proved (O = O) (trivial).
+ by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2).
+ by (λ_.trivial2) 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 (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2).
+   by (λ_.pre_base_case2) 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 (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+     by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+     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 easy2: ∀n,m. n * m = O → n = O ∨ m = O.
+ intros 2.
+ elim n 0
+  [ intro;
+    left;
+    reflexivity
+  | intro;
+    elim m 0
+    [ intros;
+      right;
+      reflexivity
+    | intros;
+      simplify in H2;
+      lapply (sym_eq ? ? ? H2);
+      elim (not_eq_O_S ? Hletin)
+    ]
+  ]
+qed.
+      
\ No newline at end of file