dyck2.v

Require Import List Arith.
Import ListNotations.

Inductive paren: Set := a | b.


(** [fill u v n na nb] :
     tries to replace unknowns in [u] to be equal to [v] (balanced) 
     
     [n] is the current difference (number of [a]'s - number of [b]'s)
     [na] is the remaining number of [a]'s still to be met 
     [nb] is the remaining number of [b]'s still to be  met 


*)
Inductive fill : 
  list (option paren) -> list paren -> nat -> nat -> nat -> Prop:=

| fill0  : fill nil nil 0 0 0 

| fill1: forall u v n na nb, 
      fill u v (S n) na nb -> fill (Some a :: u) (a::v) n (S na) nb

| fill2: forall u v n na nb, 
      fill u v (S n) na nb -> fill (None :: u) (a::v) n  na nb

| fill3: forall u v n na nb, 
      fill u v n na nb -> fill (Some b :: u) (b::v) (S n) na (S nb)

| fill4 : forall u v n na nb,
      fill u v n na nb -> fill (None :: u) (b:: v) (S n) na nb.

Goal fill [Some a; None; None; Some b] [a;b;a;b] 0 1 1.
 repeat constructor. 
 Qed.

Goal fill [Some a; None; None; Some b] [a;a;b;b] 0 1 1.
repeat constructor. 
Qed.

Goal fill [Some a; None; None] [a;b;b] 0 1 0. 
repeat constructor. 
Abort. 

Definition opt_dec (x y : option paren) :
  {x = y}+ {x <> y}.
 decide equality. 
 decide equality. 
Defined. 

Definition try_to_fill u v :=
  let nA := count_occ opt_dec u (Some a) in
  let nB := count_occ opt_dec u (Some b) in
  fill u v 0 nA nB.

Goal try_to_fill  [Some a; None; None; Some b] [a;a;b;b]. 
  red. simpl. 
  repeat constructor. 
Qed. 

Goal try_to_fill  [Some a; None; None; Some b] [a;b;a;b]. 
  red. simpl. 
  repeat constructor. 
Qed. 

Goal try_to_fill  [Some a; Some b; Some b; Some a] [a;b;b;a]. 
  red. simpl. 
  repeat constructor. 
Abort. 

Goal exists l n, fill [Some a; None; None; Some b] l n  1 1.
  eexists. eexists. 
  econstructor 2.
     econstructor 5.        
     econstructor. 
     econstructor. 
     econstructor. 
Qed.