a bug in backchain?
19 views
Skip to first unread message
Gopalan Nadathur
May 14, 2018, 11:26:04 AM5/14/18
to Abella
Looks like backchain is forgetting the annotation on atomic goals when matching. This does not seem to be correct as the following development and "proof" shows:
Type q prop.
Define p : prop by
p := true.
Theorem cont : p -> q.
induction on 1. intros. assert p. backchain IH. backchain H2.
Define p : prop by
p := true.
Theorem cont : p -> q.
induction on 1. intros. assert p. backchain IH. backchain H2.
Kaustuv Chaudhuri
May 14, 2018, 12:05:13 PM5/14/18
to Abella
Thanks for the report. This is now fixed.
Kaustuv
Reply all
Reply to author
Forward
0 new messages