f7a7f0b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some proofs in nat.idr

commitf7a7f0b87fbbb3a85f7ec74af4ba469db61cc314 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 31 Oct 2011, 17:45 (15 years ago) parent7b1336b

3 files changed+40−23

compare with master

unifiedsplit

lib/nat.idr+15 src/Idris/ElabDecls.hs+24−22 src/Idris/Prover.hs+1−1

lib/nat.idr+15

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

1+import builtins;

23data Nat = O | S Nat;

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

1213plusnO O = refl;

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

1415

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

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

389389 movelast h

390390 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

392392 elab' (PElabError e) = fail e

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

394394

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

422422

423423-- Running tactics directly

424424

425−runTac :: PTactic -> Elab ()

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

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

428− solveAll

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

430− solveAll

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

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

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

434− -- start_unify h

435− claim tyn (RSet 0)

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

437− claim valn (Var tyn)

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

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

440− focus valn

441− elab toplevel False tm

442− rewrite (Var letn)

443−runTac (Focus n) = focus n

444−runTac Solve = solve

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

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

426+runTac autoSolve = runT where

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

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

429+ when autoSolve solveAll

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

431+ when autoSolve solveAll

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

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

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

435+ -- start_unify h

436+ claim tyn (RSet 0)

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

438+ claim valn (Var tyn)

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

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

441+ focus valn

442+ elab toplevel False tm

443+ rewrite (Var letn)

444+ when autoSolve solveAll

445+ runT (Focus n) = focus n

446+ runT Solve = solve

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

446448

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

src/Idris/Prover.hs+1−1

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

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

103103 return (False, e, True, prf)

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

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

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

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

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

108108 return (False, e, False, prf))