mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-11 02:01:36 +03:00
Merge pull request #316 from ohad/fancy-preorder-reasoning
Fancy preorder reasoning
This commit is contained in:
Ohad Kammar
GitHub
commit
59588a3f3a
@ -33,36 +33,25 @@ length xs = length_aux xs Z
|
||||
|
||||
export
|
||||
length_ext : (xs : List a) -> Data.List.length xs = Data.List.TailRec.length xs
|
||||
length_ext xs = Calculate [
|
||||
Data.List.length xs
|
||||
==| sym (plusZeroRightNeutral (Data.List.length xs)),
|
||||
Data.List.length xs + 0
|
||||
==| lemma 0 xs,
|
||||
Data.List.TailRec.length_aux xs 0
|
||||
==| Refl,
|
||||
Data.List.TailRec.length xs
|
||||
==| QED
|
||||
]
|
||||
length_ext xs = Calc $
|
||||
|~ Data.List.length xs
|
||||
~~ Data.List.length xs + 0 ...( sym $ plusZeroRightNeutral $ Data.List.length xs )
|
||||
~~ Data.List.TailRec.length_aux xs 0 ...( lemma 0 xs )
|
||||
~~ Data.List.TailRec.length xs ...( Refl )
|
||||
where
|
||||
lemma : (n : Nat) -> (xs : List a) ->
|
||||
Data.List.length xs + n = length_aux xs n
|
||||
lemma n [] = Refl
|
||||
lemma n (_ :: xs) =
|
||||
let length_xs : Nat
|
||||
length_xs = Data.List.length xs in
|
||||
Calculate [
|
||||
1 + (length_xs + n)
|
||||
length_xs = Data.List.length xs in
|
||||
Calc $
|
||||
|~ 1 + (length_xs + n)
|
||||
-- Hopefully we could Frex these two steps one day
|
||||
==| plusAssociative 1 length_xs n ,
|
||||
(1 + length_xs) + n
|
||||
==| cong (+n) (plusCommutative 1 length_xs) ,
|
||||
(length_xs + 1) + n
|
||||
==| sym (plusAssociative length_xs 1 n),
|
||||
(length_xs) + (1 + n)
|
||||
==| lemma (1 + n) xs,
|
||||
length_aux xs (1 + n)
|
||||
==| QED
|
||||
]
|
||||
~~ (1 + length_xs) + n ...( plusAssociative 1 length_xs n )
|
||||
~~ (length_xs + 1) + n ...( cong (+n) (plusCommutative 1 length_xs) )
|
||||
~~ (length_xs) + (1 + n) ...( sym (plusAssociative length_xs 1 n) )
|
||||
~~ length_aux xs (1 + n) ...( lemma (1 + n) xs )
|
||||
|
||||
take_aux : Nat -> List a -> List a -> List a
|
||||
take_aux Z xs acc = reverseOnto [] acc
|
||||
@ -77,16 +66,11 @@ export
|
||||
take_ext :
|
||||
(n : Nat) -> (xs : List a) ->
|
||||
Data.List.take n xs = Data.List.TailRec.take n xs
|
||||
take_ext n xs = Calculate [
|
||||
Data.List.take n xs
|
||||
==| Refl ,
|
||||
reverse [] ++ (Data.List.take n xs)
|
||||
==| sym (revOnto (Data.List.take n xs) []) ,
|
||||
reverseOnto (Data.List.take n xs) []
|
||||
==| sym (lemma n xs []) ,
|
||||
take_aux n xs []
|
||||
==| QED
|
||||
]
|
||||
take_ext n xs = Calc $
|
||||
|~ Data.List.take n xs
|
||||
~~ reverse [] ++ (Data.List.take n xs) ...( Refl )
|
||||
~~ reverseOnto (Data.List.take n xs) [] ...( sym (revOnto (Data.List.take n xs) []) )
|
||||
~~ take_aux n xs [] ...( sym (lemma n xs []) )
|
||||
where
|
||||
lemma : (n : Nat) -> (xs, acc : List a) ->
|
||||
take_aux n xs acc = reverseOnto (Data.List.take n xs) acc
|
||||
@ -249,12 +233,10 @@ mergeReplicate_ext : (sep : a) -> (xs : List a) -> (acc : List a) ->
|
||||
mergeReplicate_aux sep xs acc =
|
||||
reverseOnto (mergeReplicate sep xs) acc
|
||||
mergeReplicate_ext sep [] acc = Refl
|
||||
mergeReplicate_ext sep (x::xs) acc = Calculate [
|
||||
mergeReplicate_aux sep xs (x :: sep :: acc)
|
||||
==| mergeReplicate_ext sep xs (x :: sep :: acc) ,
|
||||
reverseOnto (sep :: x :: mergeReplicate sep xs) acc
|
||||
==| QED
|
||||
]
|
||||
mergeReplicate_ext sep (x::xs) acc = Calc $
|
||||
|~ mergeReplicate_aux sep xs (x :: sep :: acc)
|
||||
~~ reverseOnto (sep :: x :: mergeReplicate sep xs) acc
|
||||
...( mergeReplicate_ext sep xs (x :: sep :: acc) )
|
||||
|
||||
export
|
||||
intersperse : a -> List a -> List a
|
||||
@ -314,9 +296,10 @@ mergeByOnto : List a -> (a -> a -> Ordering) -> List a -> List a -> List a
|
||||
mergeByOnto acc order [] right = reverseOnto right acc
|
||||
mergeByOnto acc order left [] = reverseOnto left acc
|
||||
mergeByOnto acc order left@(x::xs) right@(y::ys) =
|
||||
case order x y of
|
||||
LT => mergeByOnto (x :: acc) order xs right
|
||||
_ => mergeByOnto (y :: acc) order left ys
|
||||
-- We need the variant annotations (bug #300)
|
||||
case order x y of
|
||||
LT => mergeByOnto (x :: acc) order (assert_smaller left xs) right
|
||||
_ => mergeByOnto (y :: acc) order left (assert_smaller right ys)
|
||||
|
||||
mergeByOnto_ext : (acc : List a)
|
||||
-> (order : a -> a -> Ordering)
|
||||
@ -324,7 +307,9 @@ mergeByOnto_ext : (acc : List a)
|
||||
-> reverseOnto (mergeBy order left right) acc
|
||||
= mergeByOnto acc order left right
|
||||
mergeByOnto_ext acc order [] right = Refl
|
||||
mergeByOnto_ext acc order left [] = ?bug139
|
||||
mergeByOnto_ext acc order left [] with( left)
|
||||
mergeByOnto_ext acc order _ [] | [] = Refl
|
||||
mergeByOnto_ext acc order _ [] | (_::_) = Refl
|
||||
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) with (order x y)
|
||||
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | LT =
|
||||
mergeByOnto_ext (x :: acc) order xs (y::ys)
|
||||
@ -368,27 +353,31 @@ export
|
||||
sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
|
||||
sortBy cmp [] = []
|
||||
sortBy cmp [x] = [x]
|
||||
sortBy cmp xs = let (x, y) = sortBy_split xs in
|
||||
sortBy cmp zs = let (xs, ys) = sortBy_split zs in
|
||||
Data.List.TailRec.mergeBy cmp
|
||||
(Data.List.TailRec.sortBy cmp (assert_smaller xs x))
|
||||
(Data.List.TailRec.sortBy cmp (assert_smaller xs y))
|
||||
(Data.List.TailRec.sortBy cmp (assert_smaller zs xs))
|
||||
(Data.List.TailRec.sortBy cmp (assert_smaller zs ys))
|
||||
|
||||
|
||||
{-- -- This code seems to make Idris2 loop
|
||||
{- Can't really finish this proof because Data.List doesn't export the definition of sortBy. -}
|
||||
{-
|
||||
export
|
||||
sortBy_ext : (cmp : a -> a -> Ordering) -> (xs : List a) ->
|
||||
Data.List.sortBy cmp xs = Data.List.TailRec.sortBy cmp xs
|
||||
sortBy_ext cmp [] = Refl
|
||||
sortBy_ext cmp [x] = Refl
|
||||
sortBy_ext cmp xs@(y::ys) = let (x, y) = split xs in
|
||||
Calculate [
|
||||
Data.List.mergeBy cmp
|
||||
(Data.List.sortBy cmp (assert_smaller xs x))
|
||||
(Data.List.sortBy cmp (assert_smaller xs y))
|
||||
==| ?help1 ,
|
||||
sortBy_ext cmp [] = Refl
|
||||
sortBy_ext cmp [x] = Refl
|
||||
sortBy_ext cmp zs'@(z::zs) =
|
||||
Calc $
|
||||
|~ Data.List.sortBy cmp (z::zs)
|
||||
~~ (let (xs, ys) = sortBy_split zs' in
|
||||
Data.List.mergeBy cmp
|
||||
(Data.List.sortBy cmp xs)
|
||||
(Data.List.sortBy cmp ys))
|
||||
...( ?help0 )
|
||||
~~
|
||||
let (xs, ys) = sortBy_split (z::zs) in
|
||||
Data.List.TailRec.mergeBy cmp
|
||||
(Data.List.TailRec.sortBy cmp (assert_smaller xs x))
|
||||
(Data.List.TailRec.sortBy cmp (assert_smaller xs y))
|
||||
==| QED
|
||||
]
|
||||
--}
|
||||
(Data.List.TailRec.sortBy cmp xs)
|
||||
(Data.List.TailRec.sortBy cmp ys)
|
||||
...( ?help1 )
|
||||
-}
|
||||
|
||||
@ -1,42 +1,37 @@
|
||||
||| Until Idris2 starts supporting the 'syntax' keyword, here's a
|
||||
||| poor-man's equational reasoning
|
||||
||| Until Idris2 starts supporting the 'syntax' keyword, here's a
|
||||
||| poor-man's equational reasoning
|
||||
module Syntax.PreorderReasoning
|
||||
|
||||
||| Deep embedding of equation derivation sequences.
|
||||
||| Using the Nil, (::) constructors lets us use list syntax.
|
||||
infixl 0 ~~
|
||||
prefix 1 |~
|
||||
infix 1 ...
|
||||
|
||||
|||Slightly nicer syntax for justifying equations:
|
||||
|||```
|
||||
||| |~ a
|
||||
||| ~~ b ...( justification )
|
||||
|||```
|
||||
|||and we can think of the `...( justification )` as ASCII art for a thought bubble.
|
||||
public export
|
||||
data Derivation : (x : a) -> (y : b) -> Type where
|
||||
Nil : Derivation x x
|
||||
(::) : (x = y) -> Derivation y z -> Derivation x z
|
||||
(...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z)
|
||||
(...) x pf = (x ** pf)
|
||||
|
||||
public export
|
||||
data FastDerivation : (x : a) -> (y : b) -> Type where
|
||||
(|~) : (x : a) -> FastDerivation x x
|
||||
(~~) : FastDerivation x y -> (step : (z : c ** y ~=~ z)) -> FastDerivation x z
|
||||
|
||||
infix 1 ==|
|
||||
public export
|
||||
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x ~=~ y
|
||||
Calc (|~ x) = Refl
|
||||
Calc {y} ((~~) {z=y} {y=y} der (y ** Refl)) = Calc der
|
||||
|
||||
||| Explicate the term under consideration and the justification for
|
||||
||| the next step.
|
||||
export
|
||||
(==|) : (x : a) -> (x = y) -> x = y
|
||||
(==|) x pf = pf
|
||||
|
||||
||| Finishg the derivation.
|
||||
||| A bit klunky, but this /is/ a poor-man's version.
|
||||
export
|
||||
QED : {x : a} -> x = x
|
||||
QED = Refl
|
||||
|
||||
export
|
||||
Calculate : Derivation x y -> x = y
|
||||
Calculate [] = Refl
|
||||
Calculate (Refl :: der) = Calculate der
|
||||
|
||||
{--
|
||||
||| Requires Data.Nata
|
||||
{- -- requires import Data.Nat
|
||||
0
|
||||
example : (x : Nat) -> (x + 1) + 0 = 1 + x
|
||||
example x = Calculate [
|
||||
(x + 1) + 0
|
||||
==| plusZeroRightNeutral (x + 1) ,
|
||||
x + 1
|
||||
==| plusCommutative x 1 ,
|
||||
1 + x
|
||||
==| QED
|
||||
]
|
||||
--}
|
||||
example x =
|
||||
Calc $
|
||||
|~ (x + 1) + 0
|
||||
~~ x+1 ...( plusZeroRightNeutral $ x + 1 )
|
||||
~~ 1+x ...( plusCommutative x 1 )
|
||||
-}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user