X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fesempio.ma;h=8f9604a8524817acdbc1489a7613b43239981310;hb=d6ba7f4b8fbd98f2f1c848857022ef5fba80db53;hp=4005ee98ac2a187b441f06556473fbfbf3594579;hpb=189cd88a0532779547e8c10ff6f78ca93aae363a;p=helm.git

diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma
index 4005ee98a..8f9604a85 100644
--- a/helm/software/components/ng_refiner/esempio.ma
+++ b/helm/software/components/ng_refiner/esempio.ma
@@ -15,21 +15,57 @@
 include "nat/plus.ma".
 
 definition hole : ∀A:Type.A → A ≝ λA.λx.x.
+definition id : ∀A:Type.A → A ≝ λA.λx.x.
 
-inductive pippo (T:Type) (x:T) : Prop ≝ . 
+(* Common case in dama, reduction with metas
+inductive list : Type := nil : list | cons : nat -> list -> list.
+let rec len l := match l with [ nil => O | cons _ l => S (len l) ].
+axiom lt : nat -> nat -> Prop.
+axiom foo : ∀x. Not (lt (hole ? x) (hole ? O)) = (lt x (len nil) -> False).
+*) 
 
-axiom A: Type. 
-axiom B:A.
+(* meta1 Vs meta2 with different contexts
+axiom foo: 
+  ∀P:Type.∀f:P→P→Prop.∀x:P.
+   (λw. ((∀e:P.f x (w x)) = (∀y:P. f x (hole ? y)))) 
+   (λw:P.hole ? w). 
+*)
 
-axiom foo : \forall x: (hole ? A).pippo (hole ? A) x.
+(* meta1 Vs meta1 with different local contexts
+axiom foo: 
+  ∀P:Type.∀f:P→P→P.∀x,y:P. 
+    (λw.(f x (w x) = f x (w y))) (λw:P.hole ? w).
+*)
 
-axiom foo: (λx,y:A. pippo (hole ? A) x y) 
-           (hole ? B) (hole ? B).
+(* meta Vs term && term Vs meta with different local ctx
+axiom foo: 
+  ∀P:Type.∀f:P→P→P.∀x,y:P.
+    (λw.(f (w x) (hole ? x) = f x (w y))) (λw:P.hole ? w).
+*)
 
-axiom foo: λx:(hole ? Type).λy:(hole ? Type). pippo (hole ? Type) x y.
+(* occur check
+axiom foo: 
+  ∀P:Type.∀f:P→P→P.∀x,y:P.
+    (λw.(f x (f (w x) x) = f x (w y))) (λw:P.hole ? w).
+*)
 
+(* unifying the type of (y ?) with (Q x) we instantiate ? to x
+axiom foo: 
+  ∀P:Type.∀Q:P→Type.∀f:∀x:P.Q x→P→P.∀x:P.∀y:∀x.Q x.
+    (λw.(f w (y w) x = (id ? f) x (hole ? (y x)) x)) (hole ? x).
+*)  
+   
+alias num (instance 0) = "natural number".
+axiom foo: (100+111) = (100+110). 
+
+
+    (id ?(id ?(id ?(id ? (100+100))))) =
+    (id ?(id ?(id ?(id ? (99+100))))).[3:
+    apply (refl_eq nat (id ?(id ?(id ?(id ? (98+102+?))))));
+
+axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *)
 axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *) 
-axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *) 
+ 
 
 
 axiom foo: (λx,y.(λz. z x + z y) (λw:nat.hole ? w)) = λx,y.x. (* OK *)