From 7cae3af1996be9ac6062a8a1aa038743574679da Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Wed, 25 Aug 2010 15:09:31 +0000
Subject: Renamed file obsolete/plastic/test.lf, formerly plastic/test.lf

---
 obsolete/plastic/test.lf | 64 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 obsolete/plastic/test.lf

(limited to 'obsolete')

diff --git a/obsolete/plastic/test.lf b/obsolete/plastic/test.lf
new file mode 100644
index 00000000..7c163d3d
--- /dev/null
+++ b/obsolete/plastic/test.lf
@@ -0,0 +1,64 @@
+EXAMPLE FILE: less than or equal on Nat
+
+%---------------------------------------
+Nat
+
+> Inductive
+>	[Nat : Type]
+>	Constructors
+>	[zero : Nat]
+>	[succ : (n:Nat)Nat];
+
+> [plus [m:Nat] = E_Nat ([_:Nat]Nat) m ([_:Nat]succ) ];
+
+
+-----------------------
+Non-dependent Pi type.
+
+> Inductive
+>	[A,B:Type]
+>	[Pi_ : Type]
+>	Constructors
+>	[La_ : (f:(x:El A)El B)Pi_ ];
+
+
+application of Pi_ types, ie conversion to a dependent product.
+
+> Claim ap_ : (A,B:Type) Pi_ A B -> A -> B;
+> Intros A B f x;
+> Refine E_Pi_ ? ? ([_:?]B);
+> Refine f;
+> Intros fo;
+> Refine fo x;
+> ReturnAll;
+> ap_;
+
+
+
+%---------------------------------------
+Combined leq with if-branch - thus avoiding Boolean type.
+
+Notice that we have to prove (Pi_ Nat T) by induction on x, since we can't
+eliminate over (Nat -> T) in LF. 
+
+
+> Claim if_leq : (x,y:Nat)(T:Type)T -> T -> T;
+> Intros x y T leq not_leq;
+> Refine ap_ ? ? (ap_ ? ? ? x) y;
+
+> Refine La_;
+> Intros x1;
+> Refine E_Nat ([_:?]Pi_ Nat T) ?x_z ?x_s x1;
+> x_z Refine La_ ? ? ([_:?]leq);
+> Intros x1_ f_x1_;
+> Refine La_;
+> Intros y1;
+> Refine E_Nat ([_:?]T) ?y_z ?y_s y1;
+> y_z Refine not_leq;
+> Intros y1_ _;
+> Refine ap_ ? ? f_x1_ y1_;
+> ReturnAll;
+
+> if_leq;
+
+
-- 
cgit v1.2.3