0 | ||| N-ary congruence for reasoning
 1 | module Data.Telescope.Congruence
 2 |
 3 | import Data.Telescope.Telescope
 4 | import Data.Telescope.Segment
 5 | import Data.Telescope.SimpleFun
 6 | import Data.Telescope.Fun
 7 |
 8 | public export
 9 | congType : (delta : Segment n gamma)
10 |   -> (env1 : Left.Environment gamma) -> (sy1 : SimpleFun env1 delta Type) -> (lhs : Fun env1 delta sy1)
11 |   -> (env2 : Left.Environment gamma) -> (sy2 : SimpleFun env2 delta Type) -> (rhs : Fun env2 delta sy2)
12 |   -> Type
13 | congType []            env1 sy1 lhs  env2 sy2 rhs = lhs ~=~ rhs
14 | congType (ty :: delta) env1 sy1 lhs  env2 sy2 rhs =
15 |                          {x1 : ty env1} -> {x2 : ty env2}
16 |                       -> x1 ~=~ x2
17 |                       -> congType delta
18 |                            (env1 ** x1) (sy1 x1) (lhs x1)
19 |                            (env2 ** x2) (sy2 x2) (rhs x2)
20 |
21 | public export
22 | congSegment : {n : Nat} -> (0 delta : Segment n gamma)
23 |   ->(0 env1 : Left.Environment gamma)-> (0 sy1 : SimpleFun env1 delta Type) -> (0 lhs : Fun env1 delta sy1)
24 |   ->(0 env2 : Left.Environment gamma)-> (0 sy2 : SimpleFun env2 delta Type) -> (0 rhs : Fun env2 delta sy2)
25 |   ->(0 _ : env1 ~=~ env2)      -> (0 _ : sy1 ~=~ sy2)                 -> (0 _ : lhs ~=~ rhs)
26 |   -> congType delta env1 sy1 lhs
27 |                     env2 sy2 rhs
28 | congSegment {n = 0  } []            env sy context env sy context Refl Refl Refl = Refl
29 | congSegment {n = S n} (ty :: delta) env sy context env sy context Refl Refl Refl = recursiveCall
30 |   where
31 |     recursiveCall : {x1 : ty env} -> {x2 : ty env} -> x1 ~=~ x2
32 |                  -> congType delta (env ** x1) (sy x1) (context x1)
33 |                                    (env ** x2) (sy x2) (context x2)
34 |     recursiveCall {x1=x} {x2=x} Refl = congSegment delta
35 |                                                    (env ** x) (sy x) (context x)
36 |                                                    (env ** x) (sy x) (context x)
37 |                                                    Refl       Refl   Refl
38 |
39 | public export
40 | cong : {n : Nat} -> {0 delta : Segment n []} -> {0 sy : SimpleFun () delta Type}
41 |     -> (context : Fun () delta sy)
42 |     -> congType delta () sy context
43 |                       () sy context
44 | cong {n} {delta} {sy} context = congSegment delta ()    sy   context
45 |                                                   ()    sy   context
46 |                                                   Refl  Refl Refl
47 |