Skip to content

Instantly share code, notes, and snippets.

@Iainmon
Created November 14, 2024 05:19
Show Gist options
  • Save Iainmon/1afaec038f9792ae141add713ec5ac97 to your computer and use it in GitHub Desktop.
Save Iainmon/1afaec038f9792ae141add713ec5ac97 to your computer and use it in GitHub Desktop.
Require Import Coq.Init.Nat.
Inductive bit : Set := I | O.
Inductive bits : nat -> Set :=
| bnil : bits 0
| bcons : forall (n : nat), bit -> bits n -> bits (S n).
Arguments bcons [n] _ _.
Require Import List.
Import ListNotations.
Fixpoint from_list (l : list bit) : bits (length l) :=
match l with
| [] => bnil
| b :: l' => bcons b (from_list l')
end.
Fixpoint to_list {n : nat} (bs : bits n) : list bit :=
match bs with
| bnil => []
| bcons b bs' => b :: (to_list bs')
end.
Fixpoint bits_list (l : list nat) : bits (length l) :=
match l with
| [] => bnil
| 0 :: l' => bcons O (bits_list l')
| _ :: l' => bcons I (bits_list l')
end.
Fixpoint list_bits {n : nat} (bs : bits n) : list nat :=
match bs with
| bnil => []
| bcons O bs' => 0 :: (list_bits bs')
| bcons I bs' => 1 :: (list_bits bs')
end.
Definition my_bs := bits_list [1; 1; 0; 1; 1].
Compute my_bs.
Definition bits_length {n : nat} (bs : bits n) := n.
Definition bits_head {n : nat} (bs : bits (S n)) : bit :=
match bs with
| bcons b _ => b
end.
Definition bits_tail {n : nat} (bs : bits (S n)) : bits n :=
match bs with
| bcons _ bs' => bs'
end.
Definition bits_uncons {n : nat} (bs : bits (S n)) : bit * bits n := (bits_head bs, bits_tail bs).
Fixpoint bits_app {n m : nat} (b1 : bits n) (b2 : bits m) : bits (n + m) :=
match b1 (*in (bits n) return (bits (n + m))*) with
| bnil => b2
| bcons b b1' => bcons b (bits_app b1' b2)
end.
Definition bit_bin_op : Type := bit -> bit -> bit.
Definition bits_uncons2 {n : nat} (bs cs : bits (S n)) : (bit * bits n) * (bit * bits n) :=
match bs,cs with
| bcons b bs',bcons c cs' => ((b,bs'),(c,cs'))
end.
Check bits_uncons2.
Fixpoint bits_map {n : nat} (f : bit -> bit) (bs : bits n) : bits n :=
match bs with
| bnil => bnil
| bcons b bs' => bcons (f b) (bits_map f bs')
end.
Fixpoint zip_with {A B C : Type} (f : A -> B -> C)
(l1 : list A) (l2 : list B) : list C :=
match l1, l2 with
| [], _ => []
| _, [] => []
| x :: xs, y :: ys => f x y :: zip_with f xs ys
end.
Fixpoint zipWith {n : nat} (f : bit -> bit -> bit)
(v1 : bits n) (v2 : bits n) : bits n.
induction n.
- exact bnil.
- inversion v1. inversion v2.
rewrite <- H in * |- .
rewrite H in * |- .
apply bcons.
exact (f H0 H3).
exact (IHn H1 H4).
Defined.
Print zipWith.
(*I couldn't figure this one out. Just learned about proof mode for functions. This is great. But I suspect it will be impossible to prove things about this function. *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment