Hi
Let's assume I wanted to restrict an injective mapping
f:Fin (suc m) -> Fin (suc n)
to a mapping from Fin m to Fin n which still is injective.
The idea is to "thin" (Fin m) with that particular i:Fin (suc m) (if it
exists, it's unique because f is injective) which gets mapped to
fmax_n:Fin (suc n) by f, since fmax_n is the only element of Fin (suc n)
which doesn't "fit" into Fin n.
f' j = (f (thin i j))-1 , if (f i) = fmax_n
f' j = (f (fweak j))-1 , if (f i) /= fmax_n f. a. i:Fin (suc m)
I think i might have easily confused some of the many embeddings i use
here. But what puzzled me the most is that to dodge the case
of restricting a mapping from Fin (suc m) -> Fin zero I need a
non-structural recursive call.
------------------------------------------------------------------------
( f : Fin (suc m) -> Fin zero !
let !-----------------------------!
! lemma f : Zero )
lemma f <= case (f fz)
------------------------------------------------------------------------
( f : Fin (suc m) -> Fin (suc n) !
let !-----------------------------------!
! restrict _m _n f : Fin m -> Fin n )
...
restrict _ (suc m) _ zero f
<= case (lemma (restrict _ (suc m) _ zero f))
...
------------------------------------------------------------------------
Since non-structural calls are considered naughty in Epigram, does this
mean that if something isn't required to make sense in the end (and is
eliminated by "naught E"), you can jettison the guarantee that it ever
will make sense?
Best regards,
Sebastian
------------------------------------------------------------------------------
data Bool : * where true, false : Bool
------------------------------------------------------------------------------
( A : * ! ( a : A !
data !-------------! where !-----------------! ; (--------------!
! Maybe A : * ) ! yes a : Maybe A ) ! no : Maybe A )
------------------------------------------------------------------------------
( f : A -> B ; i : Maybe A !
let !---------------------------!
! fmap f i : Maybe B )
fmap f i <= case i
{ fmap f (yes a) => yes (f a)
fmap f no => no
}
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( m, n : Nat ! ( p : Gt m n !
data !------------! where (-------------------! ; !----------------------!
! Gt m n : * ) ! gtZ : ! ! gtS p : !
! Gt (suc m) zero ) ! Gt (suc m) (suc n) )
------------------------------------------------------------------------------
( n : Nat ! ( i : Fin n !
data !-----------! where (------------------! ; !--------------------!
! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) )
------------------------------------------------------------------------------
let (-----------------------!
! fMax _n : Fin (suc n) )
fMax _ n <= rec n
{ fMax _ n <= case n
{ fMax _ zero => fz
fMax _ (suc n) => fs fMax
}
}
------------------------------------------------------------------------------
( i : Fin n !
let !-----------------------!
! fWeak i : Fin (suc n) )
fWeak i <= rec i
{ fWeak i <= case i
{ fWeak fz => fz
fWeak (fs i) => fs (fWeak i)
}
}
------------------------------------------------------------------------------
( i : Fin n ! ( p : MaxOrWeak i !
data !-------------! where (------------------! ; !-----------------------!
! MaxOrWeak i ! ! isMax : ! ! isWeak p : !
! : * ) ! MaxOrWeak fMax ) ! MaxOrWeak (fWeak i) )
------------------------------------------------------------------------------
( i : Fin n !
let !------------------------------!
! maxOrWeak _n i : MaxOrWeak i )
maxOrWeak _ n i <= rec n
{ maxOrWeak _ n i <= case i
{ maxOrWeak _ (suc n) fz <= case n
{ maxOrWeak _ (suc zero) fz => isMax
maxOrWeak _ (suc (suc n)) fz => isWeak (maxOrWeak fz)
}
maxOrWeak _ (suc n) (fs i) <= view (maxOrWeak i)
{ maxOrWeak _ (suc (suc n)) (fs (fMax _ n)) => isMax
maxOrWeak _ (suc (suc n)) (fs (fWeak i))
=> isWeak (maxOrWeak (fs i))
}
}
}
------------------------------------------------------------------------------
( i : Fin (suc n) ; j : Fin n !
let !------------------------------!
! thin i j : Fin (suc n) )
thin i j <= rec i
{ thin i j <= case i
{ thin fz j => fs j
thin (fs i) j <= case j
{ thin (fs i) fz => fz
thin (fs i) (fs j) => fs (thin i j)
}
}
}
------------------------------------------------------------------------------
( n : Nat ; i : Fin zero !
let !-------------------------!
! magic n i : Fin n )
magic n i <= case i
------------------------------------------------------------------------------
( i : Fin (suc (suc n)) !
let !--------------------------!
! downcast i : Fin (suc n) )
downcast i <= view (maxOrWeak i)
{ downcast (fs (fMax _ n)) => fz
downcast (fWeak i) => i
}
------------------------------------------------------------------------------
( i, j : Fin n !
let !---------------!
! eq i j : Bool )
eq i j <= rec i
{ eq i j <= case i
{ eq fz j <= case j
{ eq fz fz => true
eq fz (fs j) => false
}
eq (fs i) j <= case j
{ eq (fs i) fz => false
eq (fs i) (fs j) => eq i j
}
}
}
------------------------------------------------------------------------------
( f : Fin m -> Fin n !
let !----------------------------------!
! maps2Max _m _n f : Maybe (Fin m) )
maps2Max _ m _ n f <= rec m
{ maps2Max _ m _ n f <= case m
{ maps2Max _ zero _ n f => no
maps2Max _ (suc m) _ n f <= case n
{ maps2Max _ (suc m) _ zero f => no
maps2Max _ (suc m) _ (suc n) f <= case (eq (f fMax) fMax)
{ maps2Max _ (suc m) _ (suc n) f => yes fMax
maps2Max _ (suc m) _ (suc n) f
=> fmap fs (maps2Max (lam i => f (fWeak i)))
}
}
}
}
------------------------------------------------------------------------------
( i : Maybe (Fin (suc n)) !
let !-------------------------------------------!
! lift i : Fin (suc n) -> Fin (suc (suc n)) )
lift i <= case i
{ lift (yes a) <= case a
{ lift (yes fz) => fs
lift (yes (fs a)) => thin (fs (fs a))
}
lift no => fWeak
}
------------------------------------------------------------------------------
( f : Fin (suc m) -> Fin zero !
let !-----------------------------!
! lemma f : Zero )
lemma f <= case (f fz)
------------------------------------------------------------------------------
( f : Fin (suc m) -> Fin (suc n) !
let !-----------------------------------!
! restrict _m _n f : Fin m -> Fin n )
restrict _ m _ n f <= case m
{ restrict _ zero _ n f => magic n
restrict _ (suc m) _ n f <= case n
{ restrict _ (suc m) _ zero f
<= case (lemma (restrict _ (suc m) _ zero f))
restrict _ (suc m) _ (suc n) f
=>
lam i => downcast (f ((lift (maps2Max _ (suc m) _ (suc n) f)) i))
}
}
------------------------------------------------------------------------------
