辅导留学生CS、讲解辅导CS课件程序设计、辅导CS
讲解R语言编程|辅导Python编程
Homework Assignment 6
1. In Coq: This problem deals with the property of binary trees presented in the second part of
the video recording Induction and Recursion. Run the presented Coq proof, explain it, and then
prove the statement independently by structural induction.
2. In Coq: This problem relies on chapter Lists of the SF textbook. Use Coq to prove
associativity of concatenation of lists of integers
Theorem app_assoc : ?l1 l2 l3 : natlist,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)
Compare the Coq proof with the proof by induction included in the same chapter. List all
essential similarities and differences.
3. In Coq: This problem relies on chapter Poly of the SF textbook. Explain the terminology:
Polymorphic Lists, Polymorphic Pairs, Higher-Order Functions: Filter, Map, Fold. Run selected
examples of Coq code illustrating the usage of all of these terms.
4. In Coq: This problem relies on chapter Tactics of the SF textbook. Explain the essence of
sections: The apply tactic, The apply…with… tactic, The inversion tactic, Using tactics on
Hypotheses, Varying the Induction Hypothesis, Unfolding Definitions, Using destruct on
compound Expressions. Run examples of Coq code illustrating the essentials of all of these
sections.
5. This problem relies on chapter Logic of the SF textbook. Explain the essence of sections:
Logical Connectives, Programming with Propositions, Applying Theorems to Arguments.
6. This problem relies on chapter Logic of the SF textbook. Explain the essence of section: Coq
vs. Set Theory.