I'm proving a theorem in Idris, and in the 2nd case:
theorem1 t1 t2 s (S_Trans u hyp1 hyp2) = let
(s1 ** (s2 ** (ueq, st1, st2))) = theorem1 t1 t2 u
hyp1' = rewrite ueq in hyp1
in case theorem1 s1 s2 s hyp1' of
(s1' ** (s2' ** (ueq', st1', st2'))) => (s1' ** (s2' ** (ueq', S_Trans s1 st1 st1', S_Trans s2 st2' st2)))`
hyp1
has type StSubtype s u
and ueq
has type u = StTApp s1 s2
. I would like a term hyp1'
with type StSubtype s (StTApp s1 s2)
.
For this, I tried rewrite ueq in hyp1
, which gives an error:
Error: While processing right hand side of theorem1. Rewriting
by u = StTApp s1 s2 did not change
type ?_ [locals in scope: u, t2, t1, hyp2, s, hyp1, s1, s2, ueq, st1, st2].
If I write a type annotation for hyp1'
, hyp1' : StSubtype s (StTApp s1 s2)
, it gives a similar error:
Error: While processing right hand side of theorem1. While processing right hand
side of $resolved2797,hyp1'. Rewriting by u = StTApp s1 s2 did not change
type StSubtype s (StTApp s1 s2).```
Use rewrite cong (StSubtype s) (sym ueq) in hyp1
What's sym
?
See this answer. In brief, rewrite
needs StTApp s1 s2 = u
not u = StTApp s1 s2
. sym
flips the equality.
What's cong
?
rewrite a = b in c
changes the whole of the type of c
from b
to a
. What you want is to turn StSubtype s u
into StSubtype s (StTApp s1 s2)
. You only have StTApp s1 s2 = u
(after using sym
), but need StSubtype s (StTApp s1 s2) = StSubtype s u
. With
cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b
you can add the StSubtype s
.