代写留学生CS、代做代写CS课件程序设计、代写CS-代写CS作业

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.