0
$\begingroup$

I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not?

First place (works fine):

**Goal 1:**
IHHkind1 : kind_check Δ T1 =
Some (Kind_Arrow K1 K2)
IHHkind2 : kind_check Δ T2 = Some K1
**(1 / 1)**
match kind_check Δ T1 with
| Some (Kind_Arrow K11 K0) =>
    match kind_check Δ T2 with
| Some K12 =>
    if eqb_kind K11 K12 then
Some K0 else
None
| None => None
end
| _ => None
end = Some K2

after rewrite -> IHHkind1. this becomes

match kind_check Δ T2 with
| Some K12 =>
    if eqb_kind K1 K12 then Some K2 else
None
| None => None
end = Some K2

Second place (errors):

 **Goal 1:**
 IHHkind : kind_check ((X, K1) :: Δ) T =
Some K2
**(1 / 1)**
match kind_check ((X, K1) :: Δ) T with
| Some K0 => Some (Kind_Arrow K1 K0)
| None => None
end = Some (Kind_Arrow K1 K2)

with error after doing rewrite -> IHHkind.:

Found no subterm matching "kind_check
  ((X, K1) :: Δ) T" in the current goal.
Raised at Unification.w_unify_to_subterm in file "pretyping/unification.ml", line 1995, characters 14-73

Could it have something to do with the cons operator?

$\endgroup$
3
  • $\begingroup$ This sort of things are usually very subtle to debug without more context. Probably there is some hidden information somewhere that differs between the hypothesis and the goal. But if you want more help, you'll need to give us a minimal working example that we can play with. $\endgroup$ Commented Jul 4 at 10:31
  • $\begingroup$ @MevenLennon-Bertrand I will work on it. For now: I figured out that if I remove the concatenating from the definitions of kind_check and has_kind (where the hypothesis is coming from), then the rewrite does work. $\endgroup$ Commented Jul 4 at 10:35
  • $\begingroup$ @MevenLennon-Bertrand I think the problem had to do with type Definitions. When I removed a type synonym for String there was no error anymore. A type used the following synonym: Definition binderTyname := string., while a function it was used in used just string. $\endgroup$ Commented Jul 4 at 14:09

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.