Inductive Propositions
Table of Contents
- 1. Summary
- 2. TODO Notes
- 3. TODO Exercises
- 3.1. DONE
clos_refl_trans_sym - 3.2. DONE
perm - 3.3. DONE
ev_double - 3.4. DONE
Perm3 - 3.5. DONE
le_inversion - 3.6. DONE
inversion_practice - 3.7. DONE
ev5_nonsense - 3.8. DONE
ev_sum - 3.9. DONE
ev_ev__ev - 3.10. DONE
ev_plus_plus - 3.11. DONE
ev'_ev - 3.12. DONE
Perm3_In - 3.13. DONE
Perm3_NotIn - 3.14. DONE
NotPerm3 - 3.15. DONE
le_facts - 3.16. DONE
plus_le_facts1 - 3.17. DONE
plus_le_facts2 - 3.18. DONE
lt_facts - 3.19. HOLD
leb_le - 3.20. DONE
R_provability - 3.21. HOLD
R_fact - 3.22. HOLD
subsequence - 3.23. DONE
R_provability2 - 3.24. DONE
exp_match_ex1 - 3.25. DONE
EmptyStr_not_needed - 3.26. DONE
re_not_empty - 3.27. HOLD
exp_match_ex2 - 3.28. NO
weak_pumping - 3.29. NO
pumping - 3.30. DONE
reflect_iff - 3.31. DONE
eqbP_practice - 3.32. DONE
nostutter_defn - 3.33. DONE
filter_challenge - 3.34. TODO
filter_challenge_2 - 3.35. TODO
palindromes - 3.36. TODO
palindrome_converse - 3.37. TODO
NoDup - 3.38. TODO
pigeonhole_principle - 3.39. NO
app_ne - 3.40. NO
star_ne - 3.41. NO
match_eps - 3.42. NO
match_eps_refl - 3.43. NO
derive - 3.44. NO
derive_corr - 3.45. NO
regex_match - 3.46. NO
regex_match_correct
- 3.1. DONE
- 4. TODO Scores
- 5. TODO Questions
- 6. TODO Metacognition
- 7. TODO Further Knowledge
- 8. TODO TODOs
Homepage | Previous: Logic.v | Code | Next: ProofObjects.v
Under construction.
1. Summary
This chapter introduces inductive propositions.
1.1. Terms
2. TODO Notes
2.1. Inductively Defined Propositions
2.2. Using Evidence in Proofs
Destructing and Inverting Evidence
Induction on Evidence
3. TODO Exercises
3.1. DONE clos_refl_trans_sym
1 star, standard, optional
3.2. DONE perm
1 star, standard, optional
3.3. DONE ev_double
1 star, standard
3.4. DONE Perm3
1 star, standard
3.5. DONE le_inversion
1 star, standard
3.6. DONE inversion_practice
1 star, standard
3.7. DONE ev5_nonsense
1 star, standard
3.8. DONE ev_sum
2 stars, standard
3.9. DONE ev_ev__ev
3 stars, advanced, especially useful
3.10. DONE ev_plus_plus
3 stars, standard, optional
3.11. DONE ev'_ev
4 stars, advanced, optional
3.12. DONE Perm3_In
2 stars, standard
3.13. DONE Perm3_NotIn
1 star, standard, optional
3.14. DONE NotPerm3
2 stars, standard, optional
3.15. DONE le_facts
3 stars, standard, especially useful
3.16. DONE plus_le_facts1
2 stars, standard, especially useful
3.17. DONE plus_le_facts2
2 stars, standard, especially useful
3.18. DONE lt_facts
3 stars, standard, optional
3.19. HOLD leb_le
4 stars, standard, optional
(50%) Stuck on leb_complete, the direction from le : nat * nat -> Prop to leb : nat * nat -> Bool
3.20. DONE R_provability
3 stars, standard, especially useful
3.21. HOLD R_fact
3 stars, standard, optional
(50%) Stuck on R_equiv_fR; the direction where sum x y = o implies R x y o.
3.22. HOLD subsequence
4 stars, advanced
(75%). Stuck on subseq_trans.
3.23. DONE R_provability2
2 stars, standard, optional
3.24. DONE exp_match_ex1
3 stars, standard
3.25. DONE EmptyStr_not_needed
2 stars, standard, optional
3.26. DONE re_not_empty
4 stars, standard
3.27. HOLD exp_match_ex2
4 stars, standard, optional
Attempted, stuck on last case.
3.28. NO weak_pumping
5 stars, advanced
I will be skipping the lengthy regex exercises.
3.29. NO pumping
5 stars, advanced, optional
I will be skipping the lengthy regex exercises.
3.30. DONE reflect_iff
2 stars, standard, especially useful
3.31. DONE eqbP_practice
3 stars, standard, especially useful
3.32. DONE nostutter_defn
3 stars, standard, especially useful
3.33. DONE filter_challenge
4 stars, advanced
3.34. TODO filter_challenge_2
5 stars, advanced, optional
3.35. TODO palindromes
4 stars, standard, optional
3.36. TODO palindrome_converse
5 stars, standard, optional
3.37. TODO NoDup
4 stars, advanced, optional
3.38. TODO pigeonhole_principle
4 stars, advanced, optional
3.39. NO app_ne
3 stars, standard, optional
3.40. NO star_ne
3 stars, standard, optional
3.41. NO match_eps
2 stars, standard, optional
3.42. NO match_eps_refl
3 stars, standard, optional
3.43. NO derive
3 stars, standard, optional
3.44. NO derive_corr
4 stars, standard, optional
3.45. NO regex_match
2 stars, standard, optional
3.46. NO regex_match_correct
3 stars, standard, optional