dcc09e0 · Idris-dev · git.iko.soy

lib/prelude/nat.idr+1−1

compare with master

unifiedsplit

@@ -51,7 +51,7 @@ plusnO : (m : Nat) -> m + O = m;

51plusnO O = refl;

52plusnO (S k) = eqRespS (plusnO k);

53

54−plusn_Sm : (n : Nat) -> (m : Nat) -> n + S m = S (n + m);

54+plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m);

55plusn_Sm O m = refl;

56plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);

57

src/Core/TT.hs+1

@@ -415,6 +415,7 @@ uniqueName :: Name -> [Name] -> Name

415uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

416 | otherwise = n

417

418+nextName (NS x s) = NS (nextName x) s

418nextName (MN i n) = MN (i+1) n

419nextName (MN i n) = MN (i+1) n

419nextName (UN x) = let (num', nm') = span isDigit (reverse x)

420nextName (UN x) = let (num', nm') = span isDigit (reverse x)

420 nm = reverse nm'

421 nm = reverse nm'

src/Idris/ElabTerm.hs+5−3

@@ -208,10 +208,12 @@ elab ist info pattern tcgen fn tm

208 solve

209 elab' ina Placeholder = do (h : hs) <- get_holes

210 movelast h

211− elab' ina (PMetavar n) = let n' = case namespace info of

211+ elab' ina (PMetavar n) = let n' = mkN n in

212− Just xs@(_:_) -> NS n xs

213− _ -> n in

214 do attack; defer n'; solve

212 do attack; defer n'; solve

213+ where mkN n@(NS _ _) = n

214+ mkN n = case namespace info of

215+ Just xs@(_:_) -> NS n xs

216+ _ -> n

215 elab' ina (PProof ts) = do mapM_ (runTac True ist) ts

217 elab' ina (PProof ts) = do mapM_ (runTac True ist) ts

216 elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts

218 elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts

217 elab' ina (PElabError e) = fail e

219 elab' ina (PElabError e) = fail e

src/Idris/Parser.hs+4−3

@@ -340,6 +340,7 @@ pNamespace syn =

340 return [PNamespace n (concat ds)]

341

342expandNS :: SyntaxInfo -> Name -> Name

343+expandNS syn n@(NS _ _) = n

343expandNS syn n = case syn_namespace syn of

344expandNS syn n = case syn_namespace syn of

344 [] -> n

345 [] -> n

345 xs -> NS n xs

346 xs -> NS n xs

@@ -796,9 +797,9 @@ pRHS syn n = do lchar '='; pExpr syn

796 <|> do symbol "?="; rhs <- pExpr syn;

797 <|> do symbol "?="; rhs <- pExpr syn;

797 return (PLet (UN "value") Placeholder rhs (PMetavar n'))

798 return (PLet (UN "value") Placeholder rhs (PMetavar n'))

798 <|> do reserved "impossible"; return PImpossible

799 <|> do reserved "impossible"; return PImpossible

799− where n' = case n of

800− UN x -> UN (x++"_lemma_1")

800+ where mkN (UN x) = UN (x++"_lemma_1")

801− x -> x

801+ mkN (NS x n) = NS (mkN x) n

802+ n' = mkN n

802

803

803pClause :: SyntaxInfo -> IParser PClause

804pClause :: SyntaxInfo -> IParser PClause

804pClause syn

805pClause syn

src/Idris/Prover.hs+2−2

@@ -55,8 +55,8 @@ dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no mo

55dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)

56 = do let OK ty = goalAtFocus ps

57 let OK env = envAtFocus ps

58− putStrLn $ "Other goals: " ++ show hs ++ "\n"

58+-- putStrLn $ "Other goals: " ++ show hs ++ "\n"

59− putStr $ showPs (reverse env)

59+ putStr $ "\n" ++ showPs (reverse env)

60 putStrLn $ "---------------------------------- (" ++ show nm

61 ++ ") --------"

62 putStrLn $ show h ++ " : " ++ showG ty ++ "\n"

tutorial/examples/theorems.idrnew file+38

@@ -0,0 +1,38 @@

1+

2+fiveIsFive : 5 = 5;

3+fiveIsFive = refl;

4+

5+twoPlusTwo : 2 + 2 = 4;

6+twoPlusTwo = refl;

7+

8+plusReduces : (n:Nat) -> plus O n = n;

9+plusReduces n = refl;

10+

11+plusReducesO : (n:Nat) -> n = plus n O;

12+plusReducesO O = refl;

13+plusReducesO (S k) = eqRespS (plusReducesO k);

14+

15+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m);

16+plusReducesS O m = refl;

17+plusReducesS (S k) m = eqRespS (plusReducesS k m);

18+

19+plusReducesO' : (n:Nat) -> n = plus n O;

20+plusReducesO' O = ?plusredO_O;

21+plusReducesO' (S k) = let ih = plusReducesO' k in

22+ ?plusredO_S;

23+

24+

25+---------- Proofs ----------

26+

27+plusredO_S = proof {

28+ intro;

29+ intro;

30+ rewrite ih;

31+ trivial;

32+};

33+

34+plusredO_O = proof {

35+ compute;

36+ trivial;

37+};

38+

tutorial/examples/views.idrnew file+39

@@ -0,0 +1,39 @@

1+module views;

2+

3+data Parity : Nat -> Set where

4+ even : Parity (n + n)

5+ | odd : Parity (S (n + n));

6+

7+parity : (n:Nat) -> Parity n;

8+parity O = even {n=O};

9+parity (S O) = odd {n=O};

10+parity (S (S k)) with parity k {

11+ parity (S (S (j + j))) | even ?= even {n=S j};

12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j};

13+}

14+

15+

16+natToBin : Nat -> List Bool;

17+natToBin O = Nil;

18+natToBin k with parity k {

19+ natToBin (j + j) | even = False :: natToBin j;

20+ natToBin (S (j + j)) | odd = True :: natToBin j;

21+}

22+

23+

24+---------- Proofs ----------

25+

26+views.parity_lemma_2 = proof {

27+ intro;

28+ intro;

29+ rewrite plusn_Sm j j;

30+ trivial;

31+};

32+

33+views.parity_lemma_1 = proof {

34+ intro j;

35+ intro;

36+ rewrite plusn_Sm j j;

37+ trivial;

38+};

39+

tutorial/provisional.texnew file+1

@@ -0,0 +1 @@

1+\section{Provisional Definitions}

tutorial/theorems.texnew file+1

@@ -0,0 +1 @@

1+\section{Theorem Proving}