blob: 7c163d3dbcd384dbd0de6cb7d1f1077c8e5e8707 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
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;
|
