Created
November 14, 2024 05:19
-
-
Save Iainmon/1afaec038f9792ae141add713ec5ac97 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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