[coq] fix padR in ohe.v
This commit is contained in:
parent
08d553e847
commit
168df58125
114
coq/ohe.v
114
coq/ohe.v
|
|
@ -1,15 +1,19 @@
|
|||
(* One hot encoding *)
|
||||
(*
|
||||
One hot encoding
|
||||
|
||||
Requirements:
|
||||
|
||||
- Exactly one marked bit
|
||||
- Size = n
|
||||
*)
|
||||
|
||||
From mathcomp Require Import all_ssreflect.
|
||||
Set Bullet Behavior "Strict Subproofs".
|
||||
|
||||
(* Set Implicit Arguments. *)
|
||||
|
||||
Require Import Bvector.
|
||||
|
||||
Search (Vector.t _ _ -> Vector.t _ _ -> bool).
|
||||
Print BVeq.
|
||||
Print Vector.eqb.
|
||||
About Vector.eqb.
|
||||
(* Require Import Arith. *)
|
||||
|
||||
(* Parameters: size and a flag indicating whether the mark has been made *)
|
||||
(* Valid values have flag set to true *)
|
||||
|
|
@ -22,6 +26,32 @@ Inductive t: nat -> bool -> Type :=
|
|||
|
||||
|
||||
Fixpoint eqb {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
|
||||
case (Nat.eqb n1 n2) eqn:Hneq.
|
||||
have Hn := iffLR (PeanoNat.Nat.eqb_eq n1 n2) Hneq.
|
||||
clear Hneq; rename Hn into Hneq.
|
||||
- refine (
|
||||
match o1, o2 with
|
||||
| Nil, Nil => true
|
||||
| Pad n1' b1' o1', Pad n2' b2' o2' => _
|
||||
| Mark n1' o1', Mark n2' o2' => _
|
||||
| _, _ => false
|
||||
end).
|
||||
+ case (Nat.eqb n1' n2') eqn:Hneq'.
|
||||
* have Hn := iffLR (PeanoNat.Nat.eqb_eq n1' n2') Hneq'.
|
||||
clear Hneq'; rename Hn into Hneq'.
|
||||
rewrite -Hneq' in o2'.
|
||||
exact: eqb _ _ _ _ o1' o2'.
|
||||
* exact: false.
|
||||
+ case (Nat.eqb n1' n2') eqn:Hneq'.
|
||||
* have Hn := iffLR (PeanoNat.Nat.eqb_eq n1' n2') Hneq'.
|
||||
clear Hneq'; rename Hn into Hneq'.
|
||||
rewrite -Hneq' in o2'.
|
||||
exact: eqb _ _ _ _ o1' o2'.
|
||||
* exact: false.
|
||||
- exact: false.
|
||||
Defined.
|
||||
|
||||
Fixpoint eqb' {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
|
||||
case (Nat.eqb n1 n2) eqn:Hneq.
|
||||
move/PeanoNat.Nat.eqb_spec: Hneq => Hneq.
|
||||
refine (
|
||||
|
|
@ -36,18 +66,57 @@ Fixpoint eqb {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
|
|||
+ move/PeanoNat.Nat.eqb_spec: Hneq' => Hneq'.
|
||||
rewrite -Hneq'.
|
||||
move => o1' o2'.
|
||||
exact: eqb _ _ _ _ o1' o2'.
|
||||
exact: eqb' _ _ _ _ o1' o2'.
|
||||
+ exact: (fun _ _ => false).
|
||||
- move: n1' n2' o1' o2' => n1' n2'.
|
||||
case (Nat.eqb n1' n2') eqn:Hneq'.
|
||||
+ move/PeanoNat.Nat.eqb_spec: Hneq' => Hneq'.
|
||||
rewrite -Hneq'.
|
||||
move => o1' o2'.
|
||||
exact: eqb _ _ _ _ o1' o2'.
|
||||
exact: eqb' _ _ _ _ o1' o2'.
|
||||
+ exact: (fun _ _ => false).
|
||||
- exact: false.
|
||||
Defined.
|
||||
|
||||
|
||||
|
||||
|
||||
(* move/PeanoNat.Nat.eqb_spec: Hneq => Hneq. *)
|
||||
(* refine ( *)
|
||||
(* match o1, o2 with *)
|
||||
(* | Nil, Nil => true *)
|
||||
(* | Pad n1' b1' o1', Pad n2' b2' o2' => _ *)
|
||||
(* | Mark n1' o1', Mark n2' o2' => _ *)
|
||||
(* | _, _ => false *)
|
||||
(* end). *)
|
||||
(* - move: n1' n2' o1' o2' => n1' n2'. *)
|
||||
(* case (Nat.eqb n1' n2') eqn:Hneq'. *)
|
||||
(* + Search Nat.eqb. *)
|
||||
(* (1* PeanoNat.Nat.eqb_eq *1) *)
|
||||
(* Check (EqNat.beq_nat_true_stt n1' n2'). *)
|
||||
(* Search Nat.eqb Nat.eqb. *)
|
||||
(* move: Hneq'. *)
|
||||
(* Check Nat.eqb_eq n1' n2'. *)
|
||||
(* Check (EqNat.beq_nat_true_stt n1' n2'). *)
|
||||
(* rewrite (EqNat.beq_nat_true_stt n1' n2') in Hneq'. *)
|
||||
(* move => o1' o2'. *)
|
||||
(* exact: eqb _ _ _ _ o1' o2'. *)
|
||||
(* Search (_ = _) Nat.eqb. *)
|
||||
(* Check PeanoNat.Nat.eqb_eq n1' n2'. *)
|
||||
(* rewrite (EqNat.beq_nat_true_stt n1' n2') in Hneq'. *)
|
||||
(* rewrite -(EqNat.beq_nat_true_stt n1' n2'). *)
|
||||
(* S *)
|
||||
(* + exact: (fun _ _ => false). *)
|
||||
(* - move: n1' n2' o1' o2' => n1' n2'. *)
|
||||
(* case (Nat.eqb n1' n2') eqn:Hneq'. *)
|
||||
(* + move/PeanoNat.Nat.eqb_spec: Hneq' => Hneq'. *)
|
||||
(* rewrite -Hneq'. *)
|
||||
(* move => o1' o2'. *)
|
||||
(* exact: eqb _ _ _ _ o1' o2'. *)
|
||||
(* + exact: (fun _ _ => false). *)
|
||||
(* - exact: false. *)
|
||||
(* Defined. *)
|
||||
|
||||
Fixpoint markCount_aux {n: nat} {b: bool} (a: t n b): nat :=
|
||||
match a with
|
||||
| Nil => 0
|
||||
|
|
@ -103,6 +172,11 @@ Example eg3: t 2 true := Mark (Pad Nil).
|
|||
Example eg4: t 3 true := Pad (Mark (Pad Nil)).
|
||||
Example eg5: t 4 true := Pad (Pad (Mark (Pad Nil))).
|
||||
|
||||
Compute eqb Nil Nil.
|
||||
Compute eqb (Mark Nil) Nil.
|
||||
Compute eqb (Pad (Mark Nil)) (Mark (Pad Nil)).
|
||||
Compute eqb (Pad (Mark Nil)) (Pad (Mark Nil)).
|
||||
|
||||
Compute markCount eg2.
|
||||
Compute markCount eg3.
|
||||
Compute markCount eg4.
|
||||
|
|
@ -127,7 +201,7 @@ by [].
|
|||
Defined.
|
||||
|
||||
|
||||
Fixpoint padR {n: nat} {b: bool} (a: t n b) (z: nat): t (z+n) b.
|
||||
Fixpoint padR {n: nat} {b: bool} (a: t n b) (z: nat): t (n+z) b.
|
||||
refine (
|
||||
match a with
|
||||
| Nil => _
|
||||
|
|
@ -142,25 +216,29 @@ refine (
|
|||
| S z' => _
|
||||
end
|
||||
end).
|
||||
- rewrite addn0.
|
||||
- rewrite add0n.
|
||||
exact: genPad z.
|
||||
- rewrite add0n.
|
||||
exact: (Pad a').
|
||||
- rewrite addSnnS.
|
||||
exact: padR _ _ (Pad (Pad a')) z'.
|
||||
- rewrite add0n.
|
||||
exact: Mark a'.
|
||||
- rewrite addSnnS.
|
||||
exact: padR _ _ (Pad (Mark a')) z'.
|
||||
- rewrite addn0.
|
||||
exact: (Pad a'). (* No change *)
|
||||
- rewrite -addSnnS.
|
||||
exact: padR _ _ (Pad (Pad a')) z'. (* an extra padding *)
|
||||
- rewrite addn0.
|
||||
exact: (Mark a'). (* No change *)
|
||||
- rewrite -addSnnS.
|
||||
exact: padR _ _ (Pad (Mark a')) z'.
|
||||
Defined.
|
||||
|
||||
Compute padL (Pad (Mark Nil)) 3.
|
||||
Compute padR (Pad (Mark Nil)) 3.
|
||||
Example eg8 := Eval compute in padR (Pad (Mark Nil)) 3.
|
||||
|
||||
Example eg := Eval compute in padR (Pad (Mark Nil)) 3.
|
||||
Require Import Extraction.
|
||||
Extraction Language Haskell.
|
||||
Recursive Extraction eg.
|
||||
Recursive Extraction eqb.
|
||||
Recursive Extraction eqb'.
|
||||
Recursive Extraction eg8.
|
||||
(*
|
||||
data T =
|
||||
Nil
|
||||
|
|
|
|||
Loading…
Reference in New Issue