Some experiments in generation of elimination principles.

diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index 77c709c7004ed9d4fc7ff7d4125cb51475fca645..e2adc110683f00ef9f54ca9e2df52de8bc893f26 100644 (file)
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -1,8 +1,8 @@
-TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
 dependent_guarded_bove_capretta.ma nat/nat.ma
-interactive/test5.ma 
 TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
+interactive/test5.ma 
 TPTP/Veloci/COL008-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
 record.ma 
@@ -12,8 +12,8 @@ TPTP/Veloci/COL016-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
 TPTP/Veloci/COL024-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
 TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
 TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
 constructor.ma coq.ma
@@ -59,25 +59,26 @@ paramodulation/boolean_algebra.ma coq.ma
 TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
 TPTP/Veloci/COL084-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
 TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
+TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
 inversion.ma coq.ma
 TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
-bad_tests/baseuri.ma 
 TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
+bad_tests/baseuri.ma 
 TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
 coercions.ma nat/compare.ma nat/times.ma
 TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
 TPTP/Veloci/COL013-1.p.ma logic/equality.ma
-TPTP/Veloci/COL064-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
+TPTP/Veloci/COL064-2.p.ma logic/equality.ma
 comments.ma coq.ma
 TPTP/Veloci/COL021-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
 TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
 TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
 bool.ma coq.ma
+ng_tactics.ma logic/connectives.ma nat/plus.ma
 TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
 TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
@@ -85,23 +86,22 @@ letrec.ma
 TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
-TPTP/Veloci/COL063-5.p.ma logic/equality.ma
 TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-5.p.ma logic/equality.ma
 continuationals.ma coq.ma
 TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
 fold.ma coq.ma
 TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
-a.ma 
 TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
-TPTP/Veloci/COL064-9.p.ma logic/equality.ma
 TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
+TPTP/Veloci/COL064-9.p.ma logic/equality.ma
 TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
 change.ma coq.ma
-TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
@@ -117,8 +117,8 @@ TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
 TPTP/Veloci/COL048-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
+TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-4.p.ma logic/equality.ma
@@ -130,18 +130,19 @@ TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
 TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
+ng_elim.ma 
 TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
 fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
 TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
 TPTP/Veloci/COL062-3.p.ma logic/equality.ma
 TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
 cut.ma coq.ma
-TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
 TPTP/Veloci/COL018-1.p.ma logic/equality.ma
+TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
 tinycals.ma logic/connectives.ma
 coercions_contravariant.ma logic/equality.ma nat/nat.ma
 interactive/automatic_insertion.ma 
@@ -156,19 +157,20 @@ TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
+ng_commands.ma nat/plus.ma
 TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
 paramodulation/BOO075-1.ma 
 TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
 fguidi.ma logic/connectives.ma nat/nat.ma
 TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
 TPTP/Veloci/COL083-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
 coercions_propagation.ma logic/connectives.ma nat/orders.ma
 TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
 interactive/test_instance.ma 
 TPTP/Veloci/COL012-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-2.p.ma logic/equality.ma
@@ -180,16 +182,16 @@ bad_induction.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
 color.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
-metasenv_ordering.ma coq.ma
 apply2.ma nat/nat.ma
+metasenv_ordering.ma coq.ma
 TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
 TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
 pullback.ma logic/equality.ma
 TPTP/Veloci/COL086-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
 decompose.ma logic/connectives.ma
@@ -204,12 +206,12 @@ dependent_type_inference.ma nat/nat.ma
 TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
 TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
 rewrite.ma coq.ma
-bad_tests/auto.ma coq.ma
 TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
+bad_tests/auto.ma coq.ma
 diabolic_fix.ma nat/nat.ma
 TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
 test4.ma coq.ma
@@ -218,16 +220,16 @@ TPTP/Veloci/GRP602-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
 TPTP/Veloci/COL004-3.p.ma logic/equality.ma
 TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
 apply.ma coq.ma
 TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-4.p.ma logic/equality.ma
+TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
 paramodulation.ma coq.ma
@@ -246,9 +248,9 @@ TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
 compose.ma logic/equality.ma
 TPTP/Veloci/COL025-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
-unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
 hard_refine.ma coq.ma
 letrecand.ma nat/nat.ma
+unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
 paramodulation/group.ma coq.ma
 TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
@@ -256,18 +258,17 @@ TPTP/Veloci/GRP566-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP541-1.p.ma logic/equality.ma
 decl.ma nat/orders.ma nat/times.ma
 TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
-universe_inconsistency.ma 
 mysql_escaping.ma 
 TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
+TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
 interactive/drop.ma 
 interactive/test6.ma 
 TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
-TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
 unfold.ma coq.ma
-TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
@@ -287,10 +288,10 @@ injection.ma coq.ma
 second.ma first.ma
 TPTP/Veloci/COL062-2.p.ma logic/equality.ma
 match_inference.ma 
-unifhint_simple.ma logic/equality.ma
 simpl.ma coq.ma
-TPTP/Veloci/COL063-6.p.ma logic/equality.ma
+unifhint_simple.ma logic/equality.ma
 TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-6.p.ma logic/equality.ma
 third.ma first.ma second.ma
 TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
@@ -304,8 +305,8 @@ coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma li
 TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
 multiple_inheritance.ma logic/equality.ma
 test3.ma coq.ma
-TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
+TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
 naiveparamod.ma logic/equality.ma
 TPTP/Veloci/GRP176-2.p.ma logic/equality.ma

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
new file mode 100644 (file)
index 0000000..c3b3d09
--- /dev/null
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+ninductive nat: Type ≝
+   O: nat
+ | S: nat → nat.
+
+nlet rec nat_rect (Q_: (∀ (x_1: (nat)).Type)) H_O H_S x_1 on x_1: (Q_ x_1) ≝
+ (match x_1 with [O ⇒ (H_O) | (S x_2) ⇒ (H_S x_2 (nat_rect Q_ H_O H_S x_2))]).
+
+
+nlet rec nat_rec (Q: nat → Type) H_O H_S x_1 on x_1 : Q x_1 ≝
+ match x_1 with
+  [ O ⇒ H_O
+  | S x_2 ⇒ H_S x_2 (nat_rec Q H_O H_S x_2)
+  ].
+
+naxiom P: nat → Prop.
+naxiom p: ∀m. P m.
+
+ninductive le (n:nat) (N: P n): ∀m:nat. P m → Type ≝
+   len: le n N n (p n)
+ | leS: ∀m,q.le n N m q → le n N (S m) (p (S m)).
+
+nlet rec le_rect n N (Q_: (∀ m.(∀ x_4.(∀ (x_3: (le n N m x_4)).Type)))) H_len H_leS m x_4 x_3
+ on x_3: (Q_ m x_4 x_3) ≝ 
+(match x_3 with [len ⇒ (H_len) | (leS m q x_5) ⇒ (H_leS m q x_5 (le_rect n N Q_ H_len H_leS ? ? x_5))]).
+
+
+
+nlet rec le_rec' (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?) (p2: ?) (D1:nat) (D2:P D1) (x: le n D1 D2) on x : Q D1 D2 x ≝
+ match x with
+  [ len ⇒ p1
+  | leS m q A ⇒ p2 m q A (le_rec ? Q p1 p2 ?? A)
+  ].
+
+nlet rec le_rec (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?) (p2: ?) (D1:nat) (D2:P D1) (x: le n D1 D2) on x : Q D1 D2 x ≝ ?.
+ ## [ ncases x;
+       ##[ #m; #q; #A; napply (p2 m q A (le_rec ? Q p1 p2 ?? A));
+       ##| napply p1;
+       ##]
+ ## |##*: ## skip;
+ ## ]
+nqed.
\ No newline at end of file