Note that these are often special cases and simplifications. Solves arithmetic equations over natural numbers. Otherwise, does nothing (does not fail).Ī powerful automation technique that subsumes reflexivity, assumption, discriminate and contradiction. Tries a collection of basic tactics to solve the goal. (A special case of the logical ex falso quodlibet.)Ĭhecks if the goal is trivially true or equivalent to a hypothesis, solves if so.
If we have a contradictory hypothesis not involving an equality, solves the goal. (A special case of the logical ex falso quodlibet.) If we have a contradictory hypothesis involving an equality, solves the goal. If we have a hypothesis that is equal to the goal, solves the goal. Adds the new subgoal P as the current goal. If they start with the same constructor, it generates hypotheses relating the subterms.Īdds a new hypothesis H that P is true to the goal. If hypothesis H states that e1 = e2, where e1 and e2 are expressions that start with different constructors, then inversion H completes the current subgoal. Where H is of type e 1 = e 2, replaces e 1 in the goal with e 2. Names the variables and inductive hypotheses generated by induction with the given names. X as Same as destruct but adds an inductive hypothesis to inductively defined cases. Replaces the function name with its underlying definition.Ĭonsiders all possible constructors of the term x, generating subgoals that need to be solved separately.ĭestructs x, remembers which constructor is being considered in the equality hypothesis eq. The opposite of intros, removes terms from context and quantifies over them in the goal.ĭeletes the terms n 1 through n n from the context. Introduce terms into the context, giving them Tactics Reference Coq Tactics Manipulating the Context Tactic
0 kommentar(er)
