search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Ltac pattern matching #145

Open sangholee12 opened 9 years ago

sangholee12 commented 9 years ago 
IHt1 : forall T : ty, tycheck t1 T = true -> |-t1 \in T
Heqn : tycheck t1 TBool = true

Ltac trans_to_rel_OK :=
match goal with
  H1 : forall x, ?P x = true -> ?P2 x , H2 : ?P ?X = true |-_ =>
  apply H1 in H2
end.

Ltac trans_to_rel_Fail :=
match goal with
  H1 : forall x, ?P x -> ?P2 x , H2 : ?P ?X |-_ =>
  apply H1 in H2
end.

I have some problem in using Ltac pattern matching. Under above context, applying "trans_to_rel_OK." succeeds, but if applying "trans_to_rel_Fail.", it fails with the following message : " Error: No matching clauses for match goal (use "Set Ltac Debug" for more info). "

Why do I have to write "= true," not just viewing the equality as a whole predicate?

jeehoonkang commented 9 years ago

Becuase ?P ?X is bool, not Prop. I agree with you in that Coq is too strict to reject your trans_to_rel_OK tactic to work properly, but it is how Coq works, for now..