f7a7f0b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some proofs in nat.idr

f7a7f0bEdwin Brady15 years ago

lib/nat.idr+15

compare with master

unifiedsplit

@@ -1,3 +1,4 @@

1+import builtins;

2data Nat = O | S Nat;

3data Nat = O | S Nat;

@@ -12,3 +13,17 @@ plusnO : (m : Nat) -> plus m O = m;

12plusnO O = refl;

13plusnO O = refl;

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

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

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

17+plusn_Sm O m = refl;

18+plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);

19+

20+plus_commutes : (n : Nat) -> (m : Nat) -> plus n m = plus m n;

21+plus_commutes O m = sym (plusnO m);

22+plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk;

23+

24+plus_commutes_Sk = proof {

25+ intro k,m,ih;

26+ refine sym;

27+ rewrite (sym ih);

28+ refine plusn_Sm;

29+};

src/Idris/ElabDecls.hs+24−22

@@ -388,7 +388,7 @@ elab info pattern tm = do elab' tm

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

389 movelast h

390 elab' (PMetavar n) = do attack; defer n; solve

391− elab' (PProof ts) = do mapM_ runTac ts

391+ elab' (PProof ts) = do mapM_ (runTac True) ts

392 elab' (PElabError e) = fail e

393 elab' x = fail $ "Not implemented " ++ show x

394

@@ -422,26 +422,28 @@ collectDeferred t = return t

422

423-- Running tactics directly

424

425−runTac :: PTactic -> Elab ()

425+runTac :: Bool -> PTactic -> Elab ()

426+runTac autoSolve = runT where

426−runTac (Intro xs) = mapM_ (\x -> do attack; intro x) xs

427+ runT (Intro xs) = mapM_ (\x -> do attack; intro x) xs

427−runTac (Exact tm) = do elab toplevel False tm

428+ runT (Exact tm) = do elab toplevel False tm

428− solveAll

429+ when autoSolve solveAll

429−runTac (Refine fn imps) = do ns <- apply (Var fn) imps

430+ runT (Refine fn imps) = do ns <- apply (Var fn) imps

430− solveAll

431+ when autoSolve solveAll

431−runTac (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

432+ runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

432− = do attack; -- (h:_) <- get_holes

433+ = do attack; -- (h:_) <- get_holes

433− tyn <- unique_hole (MN 0 "rty")

434+ tyn <- unique_hole (MN 0 "rty")

434− -- start_unify h

435+ -- start_unify h

435− claim tyn (RSet 0)

436+ claim tyn (RSet 0)

436− valn <- unique_hole (MN 0 "rval")

437+ valn <- unique_hole (MN 0 "rval")

437− claim valn (Var tyn)

438+ claim valn (Var tyn)

438− letn <- unique_hole (MN 0 "rewrite_rule")

439+ letn <- unique_hole (MN 0 "rewrite_rule")

439− letbind letn (Var tyn) (Var valn)

440+ letbind letn (Var tyn) (Var valn)

440− focus valn

441+ focus valn

441− elab toplevel False tm

442+ elab toplevel False tm

442− rewrite (Var letn)

443+ rewrite (Var letn)

444+ when autoSolve solveAll

443−runTac (Focus n) = focus n

445+ runT (Focus n) = focus n

444−runTac Solve = solve

446+ runT Solve = solve

445−runTac x = fail $ "Not implemented " ++ show x

447+ runT x = fail $ "Not implemented " ++ show x

446

448

447solveAll = try (do solve; solveAll) (return ())

449solveAll = try (do solve; solveAll) (return ())

src/Idris/Prover.hs+1−1

@@ -102,7 +102,7 @@ ploop d prompt prf e

102 when (not (null hs)) $ fail "Incomplete proof"

103 return (False, e, True, prf)

104 Right tac -> do (_, e) <- elabStep e saveState

105− (_, st) <- elabStep e (runTac tac)

105+ (_, st) <- elabStep e (runTac True tac)

106 return (True, st, False, prf ++ [step]))

107 (\err -> do iputStrLn (report err)

108 return (False, e, False, prf))