(*JĘZYK SŁÓW ZAWIERAJĄCYCH TYLE SAMO A CO B *)

(* Rozważmy następujący alfabet *)

Inductive alf : Set := a | b.

(* Stringiem nazwiemy element typu list alf

Zdefiniuj indukcyjną własność wf: list alf -> Prop, opisaną poniżej:

- puste słowo jest wf 
- jeśli v jest wf, to słowo a v b jest wf
- jeśli v jest wf, to słowo b v a jest wf 
- jeśli v i w są wf, to słowo vw jest wf		       

*)

Require Import List.

(* Udowodnij, że wf jest równoważne wf' i wf'' 
zdefiniowanym poniżej

Przyda się (prosta:) taktyka która doprowadza wyrażenia listowe, 
zbudowane z :: i ++ do postaci kanonicznej (czyli bez nawiasów) 
*)


Inductive wf' : list alf -> Prop :=
| wf'_nil : wf' nil
| wf'_consa: forall l1 l2 : list alf, wf' l1 -> wf' l2 -> 
            wf' (a::l1++b::l2)
| wf'_consb: forall l1 l2 : list alf, wf' l1 -> wf' l2 -> 
            wf' (b::l1++a::l2).
 

Inductive wf'' : list alf -> Prop :=
| wf''_nil : wf'' nil
| wf''_consa: forall l1 l2 : list alf, wf'' l1 -> wf'' l2 -> 
            wf'' (l1++a::l2++b::nil)
| wf''_consb: forall l1 l2 : list alf, wf'' l1 -> wf'' l2 -> 
            wf'' (l1++b::l2++a::nil).

(*Poniżej zdefiniowana jest funkcja która rozpoznaje słowa zawierające
taką sama liczbę a i b poprzez liczenie różnicy liczby wystapień a i
liczby wystąpień b. Udowodnij jej pełność i poprawność *)

Require Import ZArith.

	      
Fixpoint recognize (z:Z)(l:list alf){struct l} : bool :=
match l with
| nil => match z with 
         | Z0 => true
         | _ => false
         end
| cons a l' => recognize (Zsucc z) l'
| cons b l' => recognize (Zpred z) l'
end.


Lemma recognize_comp: forall l:list alf, wf l -> recognize 0 l = true.
Admitted.
								 
  
Lemma recognize_sound: forall l:list alf, recognize 0 l = true -> wf l. 
Admitted.
(*
Podpowiedź: zacznij od lematu, że recognize n l = true implikuje,
(wf app l_n l) gdzie l_n to lista składająca się z n liter a, gdy n
jest nieujemne i -n liter b wpp

Będą potrzebne lematy pomocnicze na temat konkatenacji list
*)  

								 
(*Drzewo binarne o węzłach AB i BA*)

  
Inductive bin : Set :=
| E : bin
| AB : bin -> bin -> bin
| BA : bin -> bin -> bin.
								 
Fixpoint bin_to_string (t:bin) : list alf :=
match t with
| E => nil
| AB u v => (bin_to_string u)++a::(bin_to_string v)++b::nil
| BA u v => (bin_to_string u)++b::(bin_to_string v)++a::nil
end.   


(*Relacja parsowania

parse_rel l1 l2 t oznacza: parsowanie stringu l1 
produkuje drzewo t i zostawia string l2
*)  

Inductive parse_rel: list alf -> list alf -> bin -> Prop :=
| parse_SaSb:forall (l1 l2 l3: list alf)(t1 t2: bin),
                     parse_rel l1 (a::l2) t1 -> 
                     parse_rel l2 (b::l3) t2 ->
                          parse_rel l1 l3 (AB t1 t2)
| parse_SbSa: forall (l1 l2 l3: list alf)(t1 t2: bin),
                     parse_rel l1 (b::l2) t1 -> 
                     parse_rel l2 (a::l3) t2 ->
                          parse_rel l1 l3 (BA t1 t2)
| parse_e: parse_rel nil nil E.


(*Poprawność relacji parsującej*)

Lemma parse_rel_sound_aux: forall (l1 l2: list alf)(t:bin),
   parse_rel l1 l2 t -> l1 = (bin_to_string t)++l2.
Admitted.

Lemma  parse_rel_sound: forall (l: list alf), 
  (exists t:bin, parse_rel l nil t) -> wf l.
Admitted.


(*****************************************************
DODATKOWE !! DODATKOWE !! DODATKOWE !! DODATKOWE !!
******************************************************) 
   

(*Funkcja parsująca:

czytam l, 
wyrazenie jest poprawne gdy przy l=nil stos s będzie pusty; 
drzewo parsowania jest wtedy na t. Wpp bląd. 

Parametr z oznacza na jaką literę z wejścia czekam 
by móc zastosować ktorąś z reguł gramatyki wf'

*)


Fixpoint parse (z:alf)(s:list bin)(t:bin)(l:list alf){struct l} : option bin :=
match l with
| nil => match s with
              | nil => Some t
              | _ => None
              end 
| cons a l' => match z, s with
               | _, nil => parse b (t::nil) E  l'
	       | b, _ => parse b (t::s) E l' 
               | a, cons t' s'=> parse a s' (BA t' t) l'
               end
| cons b l' => match z, s with
               | _, nil => parse a (t::nil) E l' 
               | a, _ => parse a (t::s) E l' 
               | b, cons t' s' => parse b s' (AB t' t) l' 
               end
end.            

                          
Lemma parse_complete: forall (l: list alf)(z:alf), 
  wf l -> parse z nil E l <> None.
Admitted.
(* Uwaga: być może lepiej używać wf' lub wf'' zamiast wf *)

  
Lemma parse_invert: forall (l: list alf)(t:bin)(z:alf), 
   parse z nil E l = Some t -> bin_to_string t = l.
Admitted.   
	
Lemma parse_sound: forall (l: list alf)(t:bin)(z:alf), 
   parse z nil E l = Some t -> wf l.
Admitted.