Lists

Search, pairs, lists, partial maps, options, bags.

• Defined an inductive type natprod for pairs of numbers.
• Introduced proofs using destruct and simplification.
  • Example: Proved surjective pairing by destructing pairs into components.

• Introduced the inductive type natlist for lists of natural numbers.
• Examples of recursive functions:
  • length: Calculate the length of a list.
  • app: Append two lists.
  • nonzeros: Filter out zeros from a list.

• Demonstrated generalizing theorems for stronger inductive hypotheses.
  • Example: Proved repeat_plus for generalized sums of repeated lists.

• Defined rev, a function to reverse lists.
• Proved properties of rev:
  • rev_length: Reversing a list does not change its length.
  • rev_involutive: Reversing a list twice gives the original list.
• Key Proof Techniques:
  • Leveraging helper lemmas such as app_length.
  • Structuring proofs with auxiliary results when stuck.

• Introduced bags as lists with additional functions:
  • count: Count occurrences of an element.
  • sum: Combine two bags.
  • add: Add an element to a bag.
  • member: Check if an element exists in a bag.
• Proof Techniques:
  • Direct reasoning with destruct.
  • Example: Proved add_inc_count (adding increases count) by case analysis.

• Explored techniques for proving list properties:
  • Example: rev_app_distr: Proved that reversing an appended list distributes over the append.
  • Used helper theorems (app_assoc, app_length) for modular reasoning.

• Introduced natoption to handle partial functions safely.
• Defined functions like nth_error and hd_error for lists with proper error handling.
• Proved equivalence between implementations:
  • Example: Related hd_error to an earlier implementation using a default value.

• Defined partial maps using an inductive type partial_map.
• Key functions:
  • update: Add or override key-value pairs.
  • find: Retrieve a value for a key.
• Proof Techniques:
  • Case analysis and rewrite.
  • Example: Proved update_eq (finding an updated key retrieves the value) using eqb_id_refl.

1. Simplification:
   • Simplify goals using simpl and reflexivity.
2. Case Analysis:
   • Analyze inductive data types using destruct.
3. Induction:
   • Apply structural induction for proofs involving recursive data structures.
4. Helper Lemmas:
   • Prove auxiliary results to support complex proofs.
5. Search:
   • Use Search to find existing results for reuse in proofs.

• Solution: Used destruct to decompose the pair and applied reflexivity.

• Solution: Used destruct to decompose the pair and applied reflexivity.

• nonzeros: Defined using match with an if statement to filter out zeros.
• oddmembers: Used a helper function odd to filter odd numbers recursively.
• countoddmembers: Used length on the result of oddmembers to count odd elements.

• Solution: Used simultaneous pattern matching on two lists (l1, l2) to interleave elements recursively.

• Solution:
  • count: Used recursion and if to count occurrences.
  • sum: Defined as app (list append).
  • add: Pre-pended the element to the bag.
  • member: Checked membership using recursion and if.

• Solution: Recursively removed the first occurrence of the given element using an if condition.

• Solution: Removed all occurrences of the given element using recursion and if.

• Solution: Used count and remove_one recursively to check if all elements of one bag are in another.

• Solution: Proved using simplification and a helper lemma for equality (n =? n = true).

• eqblist: Defined a recursive equality check for two lists.
• eqblist_refl: Proved by induction and simplification using eq_eq.

• Solution: Simplified the expression to prove that adding 1 ensures its count is non-zero.

• Solution: Generalized count_member_nonzero for any number using simplification and destruct.

• Solution: Used induction over the bag and helper lemmas for comparison (leb).

• Solution: Proved that the count of an element in the sum of two bags equals the sum of individual counts.

• Solution: Proved that every involution is injective by assuming f(f(x)) = x and using symmetry in reasoning.

• Solution: Proved injectivity of rev by reasoning about rev(rev(x)) = x.

• Solution: Returned None for an empty list and Some for the head of a non-empty list using match.

• Solution: Related hd_error to the earlier hd using destruct and simplification.

• Solution: Proved reflexivity of eqb_id using destruct and eqb_refl.

• Solution: Proved using simplification and the reflexivity of eqb_id.

• Solution: Used simplification and the hypothesis eqb_id x y = false.

What if we have infinite lists - how will Coq know whether functions over such data types terminates?

Inductive nat_stream : Type :=
  | Cons (n : nat) (s : nat_stream).

Fixpoint until_n (n : nat) (s : nat_stream) : natlist :=
  match n with
  | 0 => []
  | S n' => match s with
            | Cons x s' => x :: until n' s'
            end
  end.

Fixpoint unravel (s : nat_stream) : natlist :=
   match s with
   | Cons x s' => x :: unravel s'
   end.

Here, apparently, both until and unravel terminate (or Coq doesn’t complain). Why? I thought unravel would run infinitely since nat_stream is “infinite”? q

Back to Top