CODEWITHSUNDEEP
coqcoq-tactic
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Variant of the induction tactic that doesn't require using `remember` on subterms

Let's say I have two relations R1 and R2. If I need to solve a problem by induction over the term R1 A (R2 B C), I need to first do remember R2 B C, otherwise I lose the information that the second argument to R1 was equal to R2 B C. Is there a variant of induction that tactic that doesn't require me to deal with this?

Upvotes: 0

Views: 36

Answers (1)

Yves
Yves

Reputation: 4266

The answer is no.

The way induction works, it replaces every instance of each of the arguments with the values that appear at the same place in the inductive predicate constructors. To make this easier, the remember tactic, replaces the compound expression (R2 B C) by a variable. you can sometimes avoid this if (R2 B C) appears in your goal, but this is rare.

Upvotes: 2

Related Questions