Homework project 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.