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.
代写CS&Finance|建模|代码|系统|报告|考试
编程类：C++,JAVA ,数据库,WEB,Linux,Nodejs,JSP,Html,Prolog,Python,Haskell,hadoop算法,系统 机器学习
金融类：统计，计量，风险投资，金融工程，R语言，Python语言，Matlab，建立模型，数据分析，数据处理
服务类：Lab/Assignment/Project/Course/Qzui/Midterm/Final/Exam/Test帮助代写代考辅导
E-mail:850190831@qq.com 微信：BadGeniuscs 工作时间：无休息工作日-早上8点到凌晨3点
如果您用的手机请先保存二维码到手机里面，识别图中二维码。如果用电脑，直接掏出手机果断扫描。
