problem with Fin.Ind

[GoogleCodeExporter]

data Nat := (zero : Nat) ; (suc : Nat -> Nat)
idata Fin : Nat -> Set := (zero : (n : Nat) -> Fin ('suc n)) ; (suc : (n : Nat) 
-> Fin n -> Fin ('suc n))

If I try to write identity on Fin by pattern matching:

let (n : Nat)(i : Fin n) : Fin n
<= Fin.Ind n i

it works I get the goal:

Programming: < id^1 ('suc s) ('zero s) : Fin ('suc s) >

which I can fill in:

> = 'zero s

then I get the goal:

Programming: < id^1 ('suc s) ('suc s xf^1) : Fin ('suc s) >

which I can fill in:

define id ('suc m) ('suc m i) :=  'suc m (id m i)

But if I try to write this function:

let wk (m : Nat)(n : Nat)(f : Fin m -> Fin n)(i : Fin ('suc m)) : Fin ('suc n)

and then do:

> <= Fin.Ind m i

I get this programming problem:

Programming: < wk^1 ('suc s) n f i : Fin ('suc n) >

'i' is still just 'i'

Original issue reported on code.google.com by jmchap...@gmail.com on 4 Sep 2010 at 7:30

[GoogleCodeExporter]

Peter pointed out I'd given the wrong index. It should be:

> <= Fin.Ind ('suc m) i

But I guess it should give an error as the type of i isn't correct if you give 
the wrong value for m.

Original comment by jmchap...@gmail.com on 4 Sep 2010 at 7:56

• Added labels: ****
• Removed labels: ****

[GoogleCodeExporter]

The elaborator is very good at inserting coercions if you give it something 
that isn't type-correct, but it is less good at spotting equations that are 
impossible to solve. In particular, there is no cycle detection, so in this 
case it probably inserted a few coercions by |m == 'suc m| (or more complicated 
equations) and left them as hoping holes.

Original comment by adamgundry on 6 Sep 2010 at 8:25

• Added labels: ****
• Removed labels: ****

[GoogleCodeExporter]

This is the output in full output in case it is useful:

Let there be wk.
\ m : Nat ->
\ n : Nat ->
\ f : (Fin m -> Fin n) ->
\ i : Fin ('suc m) ->
Programming: < wk^1 m n f i : Fin ('suc n) >
wk_2.impl_2 > <= Fin.Ind m i
Eliminated and simplified.
\ m^3 : Nat ->
\ n^2 : Nat ->
\ f^2 : (Fin m^3 -> Fin n^2) ->
\ i^3 : Fin ('suc m^3) ->
\ i^2 : Nat ->
\ s : Nat ->
\ qe : :- i^2 == ((: Nat) ('suc s)) ->
\ m : Nat ->
\ n^1 : Nat ->
\ f^1 : (Fin m -> Fin n^1) ->
\ i^1 : Fin ('suc m) ->
\ n : Nat ->
\ f : (Fin ('suc s) -> Fin n) ->
\ i : Fin ('suc ('suc s)) ->
\ qsm : :- ((: Fin ('suc s)) ('zero s)) == (coe Fin ('suc ('suc s)) Fin ('suc 
s) (con [(\ s1 s2 fy -> [_ [[_ [_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch 
['zero 'suc] xe (\ yb -> :- ((s2 : Enum ['zero 'suc]) => yb == s2 => eqGreen 
Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig 
())))] yb) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD 
(Sig ())))] s2))) [(\ xe -> switch ['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 
'suc]) 'zero) == yb => eqGreen Desc ('constD (Sig ())) Desc (switchD ['zero 
'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _ 
, _]) (\ absurd -> naughtE (absurd %) (:- FF && FF && FF))]) (\ xe -> switch 
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc 
('prodD 'idD ('constD (Sig ()))) Desc (switchD ['zero 'suc] [('constD (Sig ())) 
('prodD 'idD ('constD (Sig ())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF 
&& FF && FF)) (\ _ -> [_ [_ , _] [_ _ , _] , _])])]) , _] , \ s2 s1 fy -> _] [_ 
[_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch ['zero 'suc] xe (\ yb -> :- ((s2 : 
Enum ['zero 'suc]) => yb == s2 => eqGreen Desc (switchD ['zero 'suc] [('constD 
(Sig ())) ('prodD 'idD ('constD (Sig ())))] yb) Desc (switchD ['zero 'suc] 
[('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] s2))) [(\ xe -> switch 
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'zero) == yb => eqGreen 
Desc ('constD (Sig ())) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 
'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _ , _]) (\ absurd -> naughtE 
(absurd %) (:- FF && FF && FF))]) (\ xe -> switch ['zero 'suc] xe (\ yb -> :- 
(((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc ('prodD 'idD ('constD (Sig 
()))) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig 
())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF && FF && FF)) (\ _ -> [_ 
[_ , _] [_ _ , _] , _])])]) , _] (\ s1 s2 fy -> _) _ (fy %) , _]) [_ [_ _ [_ _ 
[_ , _] , _] , _] (\ xe -> switch ['zero 'suc] xe (\ yb -> :- ((s2 : Enum 
['zero 'suc]) => yb == s2 => eqGreen Desc (switchD ['zero 'suc] [('constD (Sig 
())) ('prodD 'idD ('constD (Sig ())))] yb) Desc (switchD ['zero 'suc] [('constD 
(Sig ())) ('prodD 'idD ('constD (Sig ())))] s2))) [(\ xe -> switch ['zero 'suc] 
xe (\ yb -> :- (((: Enum ['zero 'suc]) 'zero) == yb => eqGreen Desc ('constD 
(Sig ())) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD 
(Sig ())))] yb))) [(\ _ -> [_ _ , _]) (\ absurd -> naughtE (absurd %) (:- FF && 
FF && FF))]) (\ xe -> switch ['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 
'suc]) 'suc) == yb => eqGreen Desc ('prodD 'idD ('constD (Sig ()))) Desc 
(switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] 
yb))) [(\ absurd -> naughtE (absurd %) (:- FF && FF && FF)) (\ _ -> [_ [_ , _] 
[_ _ , _] , _])])]) , _] (\ s1 s2 fy -> [_ [_ _ [_ _ [_ , _] , _] , _] [[_ [_ 
[_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch ['zero 'suc] xe (\ yb -> :- ((s2 : 
Enum ['zero 'suc]) => yb == s2 => eqGreen Desc (switchD ['zero 'suc] [('constD 
(Sig ())) ('prodD 'idD ('constD (Sig ())))] yb) Desc (switchD ['zero 'suc] 
[('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] s2))) [(\ xe -> switch 
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'zero) == yb => eqGreen 
Desc ('constD (Sig ())) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 
'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _ , _]) (\ absurd -> naughtE 
(absurd %) (:- FF && FF && FF))]) (\ xe -> switch ['zero 'suc] xe (\ yb -> :- 
(((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc ('prodD 'idD ('constD (Sig 
()))) Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig 
())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF && FF && FF)) (\ _ -> [_ 
[_ , _] [_ _ , _] , _])])]) , _] (\ s1 s2 fy -> [_ [(impl.eif.hope^4 ('suc s) n 
f i s1^1 s2^1 fy^1 s1 s2 fy) , impl.eif.hope^3 ('suc s) n f i s1^1 s2^1 fy^1 s1 
s2 fy] , _]) , _] [_ [_ [_ _ [_ _ [_ , _] , _] , _] (\ xe -> switch ['zero 
'suc] xe (\ yb -> :- ((s2 : Enum ['zero 'suc]) => yb == s2 => eqGreen Desc 
(switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] yb) 
Desc (switchD ['zero 'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig 
())))] s2))) [(\ xe -> switch ['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 
'suc]) 'zero) == yb => eqGreen Desc ('constD (Sig ())) Desc (switchD ['zero 
'suc] [('constD (Sig ())) ('prodD 'idD ('constD (Sig ())))] yb))) [(\ _ -> [_ _ 
, _]) (\ absurd -> naughtE (absurd %) (:- FF && FF && FF))]) (\ xe -> switch 
['zero 'suc] xe (\ yb -> :- (((: Enum ['zero 'suc]) 'suc) == yb => eqGreen Desc 
('prodD 'idD ('constD (Sig ()))) Desc (switchD ['zero 'suc] [('constD (Sig ())) 
('prodD 'idD ('constD (Sig ())))] yb))) [(\ absurd -> naughtE (absurd %) (:- FF 
&& FF && FF)) (\ _ -> [_ [_ , _] [_ _ , _] , _])])]) , _] (\ s1 s2 fy -> [_ [_ 
(fy %) , _] [_ [(impl.eif.hope^2 ('suc s) n f i s1^1 s2^1 fy^1 s1 s2 fy) , 
impl.eif.hope^1 ('suc s) n f i s1^1 s2^1 fy^1 s1 s2 fy] , _] , _]) , _] , _] , 
_]) , impl.eif.hope ('suc s) n f i %]) i) ->
Programming: < wk^1 ('suc s) n f i : Fin ('suc n) >

Original comment by jmchap...@gmail.com on 6 Sep 2010 at 10:26

• Added labels: ****
• Removed labels: ****