TaskUse these 2 theorems to prove a theorem:Keywords: pattern matching, goal, tactic, rewriteWhat is goal?goal is the theorem we want to prove in current context, like in this exampleforall p : nat, p × 1 = pintrosfirst, introduce a parameter pCoq automatically match the p with variable in goalrewriterewrite has 2 types: -> and <- for first case you can consider it as expand from LHS(Left Hand Side) to RHS according to the rewrited theorem.p * S O = p * O + p (rewrite theorem mult_n_Sm wit
Genghong Hu
Hi
