Require Export util.

(** [PFPL] Chapter 5: syntactic objects
    including strings and abstract syntax trees, etc.

    Written by Yu Zhang (yuzhang AT ustc.edu.cn) and her students. *)

(** Symbols and strings *)
(** Inductive definition of symbol *)
Inductive sym : Set :=
  | a : sym
  | b : sym
  | c : sym
  | d : sym
  | e : sym
  | f : sym
  | g : sym
  | h : sym
  | i : sym
  | j : sym
  | k : sym
  | l : sym
  | m : sym
  | n : sym
  | o : sym
  | p : sym
  | q : sym
  | r : sym
  | s : sym
  | t : sym
  | u : sym
  | v : sym
  | w : sym
  | x : sym
  | y : sym
  | z : sym.

(** Symbol equality.
    There are two ways to express the equality relation between 
    two symbols 'c1' and 'c2': 
    1) using c1 = c2 directly, but it's 'Prop' type. 
    In many situations we need a 'bool' type, so we can define it
    in this way:
    2) as a fixpoint function, and return 'bool' value. *)

(** 1) Inductive definition of symbol equality. *)
Inductive sym_eq_prop: sym -> sym -> Prop :=
  | a_eq_a : sym_eq_prop a a
  | b_eq_b : sym_eq_prop b b
  | c_eq_c : sym_eq_prop c c
  | d_eq_d : sym_eq_prop d d
  | e_eq_e : sym_eq_prop e e
  | f_eq_f : sym_eq_prop f f
  | g_eq_g : sym_eq_prop g g
  | h_eq_h : sym_eq_prop h h
  | i_eq_i : sym_eq_prop i i
  | j_eq_j : sym_eq_prop j j
  | k_eq_k : sym_eq_prop k k
  | l_eq_l : sym_eq_prop l l
  | m_eq_m : sym_eq_prop m m
  | n_eq_n : sym_eq_prop n n
  | o_eq_o : sym_eq_prop o o
  | p_eq_p : sym_eq_prop p p
  | q_eq_q : sym_eq_prop q q
  | r_eq_r : sym_eq_prop r r 
  | s_eq_s : sym_eq_prop s s
  | t_eq_t : sym_eq_prop t t
  | u_eq_u : sym_eq_prop u u
  | v_eq_v : sym_eq_prop v v
  | w_eq_w : sym_eq_prop w w
  | x_eq_x : sym_eq_prop x x
  | y_eq_y : sym_eq_prop y y
  | z_eq_z : sym_eq_prop z z.

(** 2) Fixpoint definition of symbol equality. *)
Fixpoint sym_eq_fix (c1 c2: sym) {struct c1} : bool := 
  match c1, c2 with
  | a, a => true
  | b, b => true
  | c, c => true
  | d, d => true
  | e, e => true
  | f, f => true
  | g, g => true
  | h, h => true
  | i, i => true
  | j, j => true
  | k, k => true
  | l, l => true
  | m, m => true
  | n, n => true
  | o, o => true
  | p, p => true
  | q, q => true
  | r, r => true
  | s, s => true
  | t, t => true
  | u, u => true
  | v, v => true
  | w, w => true
  | x, x => true
  | y, y => true
  | z, z => true
  | _, _ => false
  end.

(** Inductive definition of string. *)
Inductive str:Set :=
  | estr : str
  | cstr : sym -> str -> str.

(** You can also define the string concatenation in two ways:
       fixpoint and inductive definition. *)
(** Fixpoint definition of string concatenation. *)
Fixpoint str_cat_fix (s1 s2 : str) {struct s1} : str :=
  match s1 with
  | estr => s2
  | cstr sym s1' => cstr sym (str_cat_fix s1' s2)
  end.

Notation "s1 ^ s2" := (str_cat_fix s1 s2).

(** Define some lemmas to test whether fixpoint 'str_cat_fix' is 
    well-defined. Each lemma should be proved. *)
Lemma test_str_cat_fix_1 : 
  (cstr a estr) ^ (cstr b estr) = cstr a (cstr b estr).
Proof. simpl. reflexivity. Qed.

Lemma test_str_cat_fix_2 : 
  (cstr a (cstr b estr)) ^ (cstr c (cstr d estr)) = 
    cstr a (cstr b (cstr c (cstr d estr))).
Proof. simpl. reflexivity. Qed.

Lemma test_str_cat_fix_3 :
  (cstr a (cstr b (cstr c estr))) ^ (cstr d estr) = 
    cstr a (cstr b (cstr c (cstr d estr))).
Proof.
(** EXERCISE: Complete the proof. *)
(** Solution *)
  simpl. reflexivity.
Qed.

(** Inductive definition of string concatenation. *)
Inductive str_cat_prop : str -> str -> str -> Prop :=
  | cat_estr : forall s: str, 
      str_cat_prop estr s s
  | cat_cstr : forall (s1 s2 s : str) (c : sym),
      str_cat_prop s1 s2 s ->
      str_cat_prop (cstr c s1) s2 (cstr c s).

(** Similar to lemmas 'test_str_cat_fix_*', we define some lemmas to
    test whether inductive definition 'str_cat_prop' is well-defined.
    The proofs of these lemmas also should be given. *)
Lemma test_str_cat_prop_1 : 
  str_cat_prop (cstr a estr) (cstr b estr) (cstr a (cstr b estr)).
Proof. apply cat_cstr. apply cat_estr. Qed.

Lemma test_str_cat_prop_2: 
  str_cat_prop (cstr a (cstr b estr)) (cstr c (cstr d estr)) 
    (cstr a (cstr b (cstr c (cstr d estr)))).
Proof. apply cat_cstr.  apply cat_cstr. apply cat_estr. Qed.

Lemma test_str_cat_prop_3 :
  str_cat_prop (cstr a (cstr b (cstr c estr))) (cstr d estr) 
    (cstr a (cstr b (cstr c (cstr d estr)))).
Proof.
(** EXERCISE: Complete the proof. *)
(** Solution *)
apply cat_cstr. apply cat_cstr. apply cat_cstr. apply cat_estr.
Qed.

(** Inductive definition of string eaulity. *)
Inductive str_eq_prop_1: str->str->Prop :=
  | str_eq_estr_1 : 
      str_eq_prop_1 estr estr
  | str_eq_cstr_1 : forall c1 c2 : sym, forall s1 s2 : str,
      c1 = c2 -> str_eq_prop_1 s1 s2 
      -> str_eq_prop_1 (cstr c1 s1) (cstr c2 s2).

(** EXERCISE: complete the inductive definition of the string equality
             according to the Rule (5.2) in book [PFPL].
    Hint: you need use str_cat_fix *)
Inductive str_eq_prop_2: str->str->Prop :=
(** Solution *)
  | str_eq_estr_2 : forall s : str, 
      str_eq_prop_2 (estr ^ s) s
  | str_eq_cstr_2 : forall c : sym, forall s1 s2 s: str,
      str_eq_prop_2 (s1 ^ s2) s -> 
      str_eq_prop_2 ((cstr c s1) ^ s2) (cstr c s).

(* Fixpoint definion of string equality. *)
Fixpoint str_eq_fix (s1 s2:str) {struct s1} : bool :=
  match s1 with
  | estr => 
      match s2 with 
      | estr => true
      | _    => false
      end
  | cstr c1 s1' => 
      match s2 with
      | estr => false
      | cstr c2 s2' => 
          if (sym_eq_fix c1 c2) 
          then (str_eq_fix s1' s2')
          else false
      end
  end.

(** The [rewrite] tactic
    If propsition 'H: a = b' exists in premises, and 'a' and 'b' exist 
    in the goal, you can use tactic 'rewrite H' or 'rewrite -> H' to 
    replace the occurrences of 'a' with 'b' in the goal. You can also
    use 'rewrite <- H' to replace the occurrences of 'b' with 'a' in 
    the goal. This tactic also executes some beta... reduction. *)
Lemma str_cat_same_strs_1 : forall s1 s2:str,
  s1 = s2 -> 
  (s1 ^ s2) = (s2 ^ s1).
Proof.
  intros s1 s2. intros eq. rewrite -> eq. reflexivity.
Qed.

Lemma str_cat_same_strs_2 : forall s1 s2:str,
  s1 = s2 ->
  (s1 ^ s2) = (s2 ^ s1).
Proof.
  intros s1 s2. intros eq. rewrite <- eq. reflexivity.
Qed.

Definition abc : str    := (cstr a ( cstr b ( cstr c estr))).
Definition def : str    := (cstr d ( cstr e ( cstr f estr))).
Definition abcdef : str := 
  (cstr a ( cstr b ( cstr c (cstr d (cstr e (cstr f estr)))))).

Lemma test_str_eq_prop_1: str_eq_prop_1 abc abc.
Proof. 
  (** The [unfold ident] tactic.
      The occurences of 'ident' in the goal will be replaced with 
      its definition under the beta,.. reduction. *)
  unfold abc. apply str_eq_cstr_1. reflexivity.
  apply str_eq_cstr_1. reflexivity.
  apply str_eq_cstr_1. reflexivity.
  apply str_eq_estr_1. 
Qed.

Lemma test_str_eq_fix_1: str_eq_fix abc abc = true.
Proof.
  simpl. reflexivity.
Qed.

Lemma test_str_equal_prop_2: 
  str_eq_prop_1 abcdef (str_cat_fix abc def).
Proof.
  simpl. unfold def. unfold abcdef.
  apply str_eq_cstr_1. reflexivity.
  (** The [constructor num] tactic 
      The 2-nd constructor of inductive definition 'str_eq_prop_1' 
      is 'str_eq_cstr_1'. So tactic 'constructor 2' is equal to
      'intros; apply str_eq_cstr_1'.*)
  intros; apply str_eq_cstr_1. reflexivity.
  constructor 2. reflexivity.
  constructor 2. reflexivity.
  apply str_eq_cstr_1. reflexivity.
  constructor 2. reflexivity.
  constructor 1.
Qed.

Lemma test_str_eq_fix_2: 
  str_eq_fix abcdef (str_cat_fix abc def) = true.
Proof.
  simpl. reflexivity.
Qed.

(** The [induction term] and [destruct term] tactics. *)
Lemma str_eq_self: forall s:str, str_eq_prop_1 s s.
Proof.
  (** For an inductive structure or rule, you can use [induction] tactic
      to obtain several subgoals from the goal, then give the proof of
      each subgoal. This tactic will generate the inductive terms as 
      premises automatically.
      Notice: the [destruct] tactic also split a goal into several 
      subgoals, but it does not generate the inductive terms as premises. *)
  intros. induction s0.
  (** [Case] tactic is defined in util.v by Ltac mechanism. 
      It is useful for case anlysis. *)
  Case "estr".
    constructor 1.
  Case "cstr".
    constructor 2.  reflexivity.
    (** The [assumption] tactic. 
        It looks in the local context for an hypothesis which type
        is equal to the goal.*)
    assumption.
Qed.

Fixpoint str_len_fix (str:str) {struct str} : nat :=
  match str with
  | estr        => O
  | cstr c1 s' => S (str_len_fix s')
  end.

Lemma test_str_len_1: str_len_fix abc = 3.
Proof. reflexivity. Qed.
Lemma test_str_len_2: str_len_fix estr = 0.
Proof. reflexivity. Qed.
Lemma test_str_len_3: str_len_fix (str_cat_fix abc def) = 6.
Proof. reflexivity. Qed.

(** EXERCISE: complete exercise 2 in section 5.4 of book [PFPL]. 
    Please define two lemmas which both assert that string concatenation is 
    associative, one lemma using 'str_cat_fix' and the other using 
    'str_cat_prop'.
    After definition, you should give the proof of each lemma. *)
(** Solution *)
Lemma str_cat_fix_assoc : forall s1 s2 s3 : str,
  (( s1 ^ s2 ) ^ s3 ) = ( s1 ^ ( s2 ^ s3)).
Proof. intros s1 s2 s3. induction s1. 
  Case "estr". simpl. reflexivity.
  Case "cstr". simpl. rewrite -> IHs1. reflexivity.
Qed.

Lemma str_cat_prop_assoc : forall s1 s2 s3 : str,
  forall s12 : str, str_cat_prop s1 s2 s12 ->
    forall s23 : str, str_cat_prop s2 s3 s23 ->
      forall s123 : str, str_cat_prop s12 s3 s123 ->
        forall s123' : str, str_cat_prop s1 s23 s123' ->
          s123 = s123'.
Proof. 
Admitted.