git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/test/proof002/Reflect.idr
210 lines 7.2 kB history raw
1module Reflect
3import Decidable.Equality
5%default total
7using (xs : List a, ys : List a, G : List (List a))
9 data Elem : a -> List a -> Type where
10 Stop : Elem x (x :: xs)
11 Pop : Elem x ys -> Elem x (y :: xs)
13-- Expr is a reflection of a list, indexed over the concrete list,
14-- and over a set of list variables.
16 data Expr : List (List a) -> List a -> Type where
17 App : Expr G xs -> Expr G ys -> Expr G (xs ++ ys)
18 Var : Elem xs G -> Expr G xs
19 ENil : Expr G []
21-- Reflection of list equalities, indexed over the concrete equality.
23 data ListEq : List (List a) -> Type -> Type where
24 EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys)
26-- Fully right associative list expressions
28 data RExpr : List (List a) -> List a -> Type where
29 RApp : RExpr G xs -> Elem ys G -> RExpr G (xs ++ ys)
30 RNil : RExpr G []
32-- Convert an expression to a right associative expression, and return
33-- a proof that the rewriting has an equal interpretation to the original
34-- expression.
36-- The idea is that we use this proof to build a proof of equality of
37-- list appends
39 expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))
40 expr_r ENil = (_ ** (RNil, Refl))
41 expr_r (Var i) = (_ ** (RApp RNil i, Refl))
42 expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in
43 let (yl ** (yr, yprf)) = expr_r ey in
44 appRExpr _ _ xr yr xprf yprf
45 where
46 appRExpr : (xs', ys' : List a) ->
47 {G : List (List a)} -> {xs, ys : List a} ->
48 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
49 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))
50 appRExpr x' y' rxs (RApp e i) xprf yprf
51 = let (xs ** (rec, prf)) = appRExpr _ _ rxs e Refl Refl in
52 (_ ** (RApp rec i, ?appRExpr1))
53 appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))
55 r_expr : RExpr G xs -> Expr G xs
56 r_expr RNil = ENil
57 r_expr (RApp xs i) = App (r_expr xs) (Var i)
59-- Convert an expression to some other equivalent expression (which
60-- just happens to be normalised to right associative form)
62 reduce : Expr G xs -> (xs' ** (Expr G xs', xs = xs'))
63 reduce e = let (x' ** (e', prf)) = expr_r e in
64 (x' ** (r_expr e', prf))
66-- Build a proof that two expressions are equal. If they are, we'll know
67-- that the indices are equal.
69 eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->
70 Maybe (e = e')
71 eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y')
72 eqExpr (App x y) (App x y) | (Just Refl, Just Refl) = Just Refl
73 eqExpr (App x y) (App x' y') | _ = Nothing
74 eqExpr (Var i) (Var j) with (prim__syntactic_eq _ _ i j)
75 eqExpr (Var i) (Var i) | (Just Refl) = Just Refl
76 eqExpr (Var i) (Var j) | _ = Nothing
77 eqExpr ENil ENil = Just Refl
78 eqExpr _ _ = Nothing
80-- Given a couple of reflected expressions, try to produce a proof that
81-- they are equal
83 buildProof : {xs : List a} -> {ys : List a} ->
84 Expr G ln -> Expr G rn ->
85 (xs = ln) -> (ys = rn) -> Maybe (xs = ys)
86 buildProof e e' lp rp with (eqExpr e e')
87 buildProof e e lp rp | Just Refl = ?bp1
88 buildProof e e' lp rp | Nothing = Nothing
90 testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys)
91 testEq l r = let (ln ** (l', lPrf)) = reduce l in
92 let (rn ** (r', rPrf)) = reduce r in
93 buildProof l' r' lPrf rPrf
95-- Given a reflected equality, try to produce a proof that holds
97 prove : ListEq G t -> Maybe t
98 prove (EqP xs ys) = testEq xs ys
100 getJust : (x : Maybe a) -> IsJust x -> a
101 getJust (Just p) ItIsJust = p
104-- Some helpers for later... 'prim__syntactic_eq' is a primitive which
105-- (at compile-time only) attempts to construct a proof that its arguments
106-- are syntactically equal. We'll find this useful for referring to variables
107-- in reflected terms.
109 isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
110 isElem x [] = Nothing
111 isElem x (y :: ys) with (prim__syntactic_eq _ _ x y)
112 isElem x (x :: ys) | Just Refl = [| Stop |]
113 isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]
115 weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs)
116 weakenElem [] p = p
117 weakenElem (g :: G) p = Pop (weakenElem G p)
119 weaken : (G' : List (List a)) ->
120 Expr G xs -> Expr (G' ++ G) xs
121 weaken G' (App l r) = App (weaken G' l) (weaken G' r)
122 weaken G' (Var x) = Var (weakenElem G' x)
123 weaken G' ENil = ENil
126-- Now, some reflection magic.
127-- %reflection means a function runs on syntax, rather than on constructors.
128-- So, 'reflectList' builds a reflected List expression as defined above.
130-- It also converts (x :: xs) into a reflected [x] ++ xs So that the above
131-- reduction will work the right way.
133%reflection
134reflectList : (G : List (List a)) ->
135 (xs : List a) -> (G' ** Expr (G' ++ G) xs)
136reflectList G [] = ([] ** ENil)
138reflectList G (x :: xs) with (reflectList G xs)
139 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
140 | Just p = (G' ** App (Var p) xs')
141 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
143reflectList G (xs ++ ys) with (reflectList G xs)
144 | (G' ** xs') with (reflectList (G' ++ G) ys)
145 | (G'' ** ys') = ((G'' ++ G') **
146 rewrite (sym (appendAssociative G'' G' G)) in
147 App (weaken G'' xs') ys')
148reflectList G t with (isElem t G)
149 | Just p = ([] ** Var p)
150 | Nothing = ([t] ** Var Stop)
153-- Similarly, reflectEq converts an equality proof on Lists into the ListEq
154-- reflection. Note that it isn't total, and we have to give the element type
155-- explicitly because it can't be inferred from P.
157-- This is not really a problem - we'll want different reflections for different
158-- forms of equality proofs anyway.
160%reflection
161reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
162reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
163 | (G' ** xs') with (reflectList (G' ++ G) ys)
164 | (G'' ** ys') = ((G'' ++ G') **
165 rewrite (sym (appendAssociative G'' G' G)) in
166 EqP (weaken G'' xs') ys')
169-- Need these before we can test it or the reductions won't normalise fully...
171---------- Proofs ----------
173Reflect.appRExpr1 = proof {
174 intros;
175 rewrite sym xprf;
176 rewrite sym yprf;
177 rewrite prf;
178 rewrite sym (appendAssociative xs1 xs2 ys1);
179 trivial;
182Reflect.appRExpr2 = proof {
183 intros;
184 rewrite xprf;
185 rewrite sym yprf;
186 rewrite appendNilRightNeutral x';
187 trivial;
190Reflect.bp1 = proof {
191 intros;
192 refine Just;
193 rewrite sym lp;
194 rewrite sym rp;
195 trivial;
198-- "quoteGoal x by p in e" does some magic
199-- The effect is to bind x to p applied to the current goal. If 'p' is a
200-- reflection function (which is the most likely thing to be useful...)
201-- then we can feed the result to the above 'prove' function and pull out
202-- the proof, if it exists.
204-- The syntax declaration below just gives us an easy way to invoke the
205-- prover.
207syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
208 getJust (prove (getProof x)) ItIsJust