← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/epic/tests/Forcing4.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/epic/tests/Forcing4.agda
1
 
module tests.Forcing4 where
2
 
 
3
 
open import Prelude.Nat
4
 
open import Prelude.Fin
5
 
open import Prelude.Eq
6
 
open import Prelude.String
7
 
open import Prelude.IO
8
 
open import Prelude.Unit
9
 
 
10
 
{-
11
 
toNat : {n : Nat} → Fin n → Nat
12
 
toNat (zero _)    = 0
13
 
toNat (suc _ i) = suc (toNat i)
14
 
-}
15
 
 
16
 
Rel : (X : Set) -> Set1
17
 
Rel X = X -> X -> Set
18
 
 
19
 
data _<=_ : Rel Nat where
20
 
  z<=n : ∀ n                 → Z  <= n
21
 
  s<=s : ∀ m n (m<=n : m <= n) → S m <= S n
22
 
 
23
 
_ℕ<_ : Rel Nat
24
 
m ℕ< n = S m <= n
25
 
 
26
 
 
27
 
fromℕ≤ : ∀ {m n} → m ℕ< n → Fin n
28
 
fromℕ≤ (s<=s .0 n (z<=n .n)) = fz {n}
29
 
fromℕ≤ (s<=s .(S m) .(S n) (s<=s m n m<=n)) = fs {S n} (fromℕ≤ (s<=s m n m<=n))
30
 
 
31
 
 
32
 
fromℕ≤-toℕ : ∀ m (i : Fin m) (i<m : forget i ℕ< m) → fromℕ≤ i<m == i
33
 
fromℕ≤-toℕ .(S n) (fz {n}) (s<=s .0 .n (z<=n .n)) = refl
34
 
fromℕ≤-toℕ .(S (S n)) (fs .{S n} y) (s<=s .(S (forget y)) .(S n) (s<=s .(forget y) n m≤n)) = cong (\ n -> fs n) (fromℕ≤-toℕ (S n) y (s<=s (forget y) n m≤n))
35
 
 
36
 
[_/2] : Nat -> Nat
37
 
[ 0 /2] = 0
38
 
[ 1 /2] = 0
39
 
[ S (S n) /2] = S [ n /2]
40
 
 
41
 
[1/2]-mono : (m n : Nat) -> m <= n -> [ m /2] <= [ n /2]
42
 
[1/2]-mono .0 .n (z<=n n) = z<=n [ n /2]
43
 
[1/2]-mono .1 .(S n) (s<=s .0 .n (z<=n n)) = z<=n [ S n /2]
44
 
[1/2]-mono .(S (S m)) .(S (S n)) (s<=s .(S m) .(S n) (s<=s m n m<=n)) = s<=s [ m /2] [ n /2] ([1/2]-mono m n m<=n)
45
 
 
46
 
showEq : {X : Set}{A : X}  -> A == A -> String
47
 
showEq refl = "refl"
48
 
 
49
 
show<= : {m n : Nat} -> m <= n -> String
50
 
show<= (z<=n n) = "0 <= " +S+ natToString n
51
 
show<= (s<=s m n m<=n) = natToString (S m) +S+ " <= " +S+ natToString (S n)
52
 
 
53
 
data Bot : Set where
54
 
foo : (n : Nat) -> S n <= n -> Bot
55
 
foo .(S n) (s<=s .(S n) n le) = foo n le
56
 
 
57
 
main : IO Unit
58
 
main = putStrLn (showEq (fromℕ≤-toℕ 3 (inc (inject 1)) le)) ,,
59
 
       putStrLn (show<= ([1/2]-mono 4 6 le'))
60
 
  where
61
 
    le : 2 <= 3
62
 
    le = s<=s _ _ (s<=s _ _ (z<=n _))
63
 
    le' : 4 <= 6
64
 
    le' = s<=s _ _ (s<=s _ _ (s<=s _ _ (s<=s _ _ (z<=n _))))