Last active
December 20, 2015 15:08
-
-
Save edwinb/6151593 to your computer and use it in GitHub Desktop.
Automated list associativity proofs, by reflection, in Idris.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Reflect | |
import Decidable.Equality | |
using (xs : List a, ys : List a, G : List (List a)) | |
data Elem : a -> List a -> Type where | |
Stop : Elem x (x :: xs) | |
Pop : Elem x ys -> Elem x (y :: xs) | |
-- Expr is a reflection of a list, indexed over the concrete list, | |
-- and over a set of list variables. | |
data Expr : List (List a) -> List a -> Type where | |
App : Expr G xs -> Expr G ys -> Expr G (xs ++ ys) | |
Var : Elem xs G -> Expr G xs | |
ENil : Expr G [] | |
-- Reflection of list equalities, indexed over the concrete equality. | |
data ListEq : List (List a) -> Type -> Type where | |
EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys) | |
-- Fully right associative list expressions | |
data RExpr : List (List a) -> List a -> Type where | |
RApp : RExpr G xs -> Elem ys G -> RExpr G (xs ++ ys) | |
RNil : RExpr G [] | |
-- Convert an expression to a right associative expression, and return | |
-- a proof that the rewriting has an equal interpretation to the original | |
-- expression. | |
-- The idea is that we use this proof to build a proof of equality of | |
-- list appends | |
expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs')) | |
expr_r ENil = (_ ** (RNil, refl)) | |
expr_r (Var i) = (_ ** (RApp RNil i, refl)) | |
expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in | |
let (yl ** (yr, yprf)) = expr_r ey in | |
appRExpr _ _ xr yr xprf yprf | |
where | |
appRExpr : (xs', ys' : List a) -> | |
RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) -> | |
(ws' ** (RExpr G ws', xs' ++ ys' = ws')) | |
appRExpr x' y' rxs (RApp e i) xprf yprf | |
= let (xs ** (rec, prf)) = appRExpr _ _ rxs e refl refl in | |
(_ ** (RApp rec i, ?appRExpr1)) | |
appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2)) | |
r_expr : RExpr G xs -> Expr G xs | |
r_expr RNil = ENil | |
r_expr (RApp xs i) = App (r_expr xs) (Var i) | |
-- Convert an expression to some other equivalent expression (which | |
-- just happens to be normalised to right associative form) | |
reduce : Expr G xs -> (xs' ** (Expr G xs', xs = xs')) | |
reduce e = let (x' ** (e', prf)) = expr_r e in | |
(x' ** (r_expr e', prf)) | |
-- Build a proof that two expressions are equal. If they are, we'll know | |
-- that the indices are equal. | |
eqExpr : (e : Expr G xs) -> (e' : Expr G ys) -> | |
Maybe (e = e') | |
eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y') | |
eqExpr (App x y) (App x y) | (Just refl, Just refl) = Just refl | |
eqExpr (App x y) (App x' y') | _ = Nothing | |
eqExpr (Var i) (Var j) with (prim__syntactic_eq _ _ i j) | |
eqExpr (Var i) (Var i) | (Just refl) = Just refl | |
eqExpr (Var i) (Var j) | _ = Nothing | |
eqExpr ENil ENil = Just refl | |
eqExpr _ _ = Nothing | |
-- Given a couple of reflected expressions, try to produce a proof that | |
-- they are equal | |
buildProof : {xs : List a} -> {ys : List a} -> | |
Expr G ln -> Expr G rn -> | |
(xs = ln) -> (ys = rn) -> Maybe (xs = ys) | |
buildProof e e' lp rp with (eqExpr e e') | |
buildProof e e lp rp | Just refl = ?bp1 | |
buildProof e e' lp rp | Nothing = Nothing | |
testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys) | |
testEq l r = let (ln ** (l', lPrf)) = reduce l in | |
let (rn ** (r', rPrf)) = reduce r in | |
buildProof l' r' lPrf rPrf | |
-- Given a reflected equality, try to produce a proof that holds | |
prove : ListEq G t -> Maybe t | |
prove (EqP xs ys) = testEq xs ys | |
getJust : (x : Maybe a) -> IsJust x -> a | |
getJust (Just p) ItIsJust = p | |
-- Some helpers for later... 'prim__syntactic_eq' is a primitive which | |
-- (at compile-time only) attempts to construct a proof that its arguments | |
-- are syntactically equal. We'll find this useful for referring to variables | |
-- in reflected terms. | |
isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs) | |
isElem x [] = Nothing | |
isElem x (y :: ys) with (prim__syntactic_eq _ _ x y) | |
isElem x (x :: ys) | Just refl = [| Stop |] | |
isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |] | |
weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs) | |
weakenElem [] p = p | |
weakenElem (g :: G) p = Pop (weakenElem G p) | |
weaken : (G' : List (List a)) -> | |
Expr G xs -> Expr (G' ++ G) xs | |
weaken G' (App l r) = App (weaken G' l) (weaken G' r) | |
weaken G' (Var x) = Var (weakenElem G' x) | |
weaken G' ENil = ENil | |
-- Now, some reflection magic. | |
-- %reflection means a function runs on syntax, rather than on constructors. | |
-- So, 'reflectList' builds a reflected List expression as defined above. | |
-- It also converts (x :: xs) into a reflected [x] ++ xs so that the above | |
-- reduction will work the right way. | |
%reflection | |
reflectList : (G : List (List a)) -> | |
(xs : List a) -> (G' ** Expr (G' ++ G) xs) | |
reflectList G [] = ([] ** ENil) | |
reflectList G (x :: xs) with (reflectList G xs) | |
| (G' ** xs') with (isElem (List.(::) x []) (G' ++ G)) | |
| Just p = (G' ** App (Var p) xs') | |
| Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs')) | |
reflectList G (xs ++ ys) with (reflectList G xs) | |
| (G' ** xs') with (reflectList (G' ++ G) ys) | |
| (G'' ** ys') = ((G'' ++ G') ** | |
rewrite (sym (appendAssociative G'' G' G)) in | |
App (weaken G'' xs') ys') | |
reflectList G t with (isElem t G) | |
| Just p = ([] ** Var p) | |
| Nothing = ([t] ** Var Stop) | |
-- Similarly, reflectEq converts an equality proof on Lists into the ListEq | |
-- reflection. Note that it isn't total, and we have to give the element type | |
-- explicitly because it can't be inferred from P. | |
-- This is not really a problem - we'll want different reflections for different | |
-- forms of equality proofs anyway. | |
%reflection | |
reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P) | |
reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs) | |
| (G' ** xs') with (reflectList (G' ++ G) ys) | |
| (G'' ** ys') = ((G'' ++ G') ** | |
rewrite (sym (appendAssociative G'' G' G)) in | |
EqP (weaken G'' xs') ys') | |
-- Need these before we can test it or the reductions won't normalise fully... | |
---------- Proofs ---------- | |
Reflect.appRExpr1 = proof { | |
intros; | |
rewrite sym xprf; | |
rewrite sym yprf; | |
rewrite prf; | |
rewrite sym (appendAssociative xs xs2 ys1); | |
trivial; | |
} | |
Reflect.appRExpr2 = proof { | |
intros; | |
rewrite xprf; | |
rewrite sym yprf; | |
rewrite appendNilRightNeutral x'; | |
trivial; | |
} | |
Reflect.bp1 = proof { | |
intros; | |
refine Just; | |
rewrite sym lp; | |
rewrite sym rp; | |
trivial; | |
} | |
-- "quoteGoal x by p in e" does some magic | |
-- The effect is to bind x to p applied to the current goal. If 'p' is a | |
-- reflection function (which is the most likely thing to be useful...) | |
-- then we can feed the result to the above 'prove' function and pull out | |
-- the proof, if it exists. | |
-- The syntax declaration below just gives us an easy way to invoke the | |
-- prover. | |
syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in | |
getJust (prove (getProof x)) ItIsJust | |
---- And finally, a couple of tests to show it works | |
total | |
testReflect0 : (xs, ys : List a) -> ((xs ++ (ys ++ xs)) = ((xs ++ ys) ++ xs)) | |
testReflect0 {a} xs ys = AssocProof a | |
total | |
testReflect1 : (xs, ys : List a) -> | |
((xs ++ (x :: ys ++ xs)) = ((xs ++ [x]) ++ (ys ++ xs))) | |
testReflect1 {a} xs ys = AssocProof a | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment