For example, If here is a constructor of an inductive type: Another way to think of inversion is like “opening the box”. It might also add more subgoals.Ī common use case is that you have an equation of the same constructor of an inductive type in your hypotheses and you want to say that their corresponding parts must be equal. It might add more propositions to the hypotheses. is that it asks Coq to figure out what else need to be true to make H true, where H is an inductive type. In my opinion, inversion is one of the most powerful and most frequent-used tactics. We can see that there are two induction hypotheses ( IHTransform1 and IHTransform2) because the constructor TransformIf has two recursively defined preconditions. Mathematical induction works on natrual numbers, which is a recursive-defined inductive type:Į : arith then_, else_, tthen, telse : cmd H : Transform then_ tthen H0 : Transform else_ telse IHTransform1 : transform then_ = tthen IHTransform2 : transform else_ = telse _ ( 1 / 1 ) transform ( If e then_ else_ ) = If e telse tthen Later, I found that you can think of induction as a generalization of mathematical induction. But there is no “base case” or “induction step” in induction and the number of cases is not necessarily two, depending on the inductive type. To prove a proposition P using mathematical induction, you first prove a base case P(0) and then prove a induction step P(n+1) given that P(n) holds. If a constructor calls another of the same inductive type, there will be a induction hypothesis for that.Īt first, I confused induction with mathematical induction. There are usually as many subgoals as the constructors of the inductive type. Induction is one of the most important tactics to prove things. Logically, when you know A \/ B is true, you need to discuss two cases: A is true and B is true.
Therefore, when you destruct a \/, it becomes two subgoals. Inductive or ( A B : Prop ) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B.
#COQ TACTICS FREE#
Each time it consumes a free variable in forall or a proposition before -> (a precondition). Intros introduces hypotheses in order, from the goal.
#COQ TACTICS MANUAL#
TacticsĪlthough I cannot understand most part of it, the Coq manual can still be your best friend. Before I fully forgot Coq, let me write down some beginner-level tricks I learned when doing homework, just in case you might find it useful or I come back to Coq some decades later. But I’m not a huge believer of machine-checked proof or verification. I’m quite happy that I completed Coq in my wish list.
#COQ TACTICS SOFTWARE#
#COQ TACTICS CODE#
It comes with detailed Coq code for each chapter and a very powerful Coq library frap. It’s a short textbook with big margins and lots of whitespaces.
0 kommentar(er)
