re_not_empty.v

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => true
  | App re1 re2 | Union re1 re2 => orb (re_not_empty re1) (re_not_empty re2)
  | Star re => re_not_empty re
  end.

Lemma re_not_empty_correct : forall T (re : reg_exp T),
  (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  split; intros. destruct H. induction re.
  inversion H. auto.
  auto. simpl. apply orb_true_iff.
  

  
  T : Type
  re1, re2 : reg_exp T
  x : list T
  H : x =~ App re1 re2
  IHre1 : x =~ re1 -> re_not_empty re1 = true
  IHre2 : x =~ re2 -> re_not_empty re2 = true
  ============================
  re_not_empty re1 = true \/ re_not_empty re2 = true

subgoal 2 (ID 373) is:
 re_not_empty (Union re1 re2) = true
subgoal 3 (ID 378) is:
 re_not_empty (Star re) = true
subgoal 4 (ID 327) is:
 exists s : list T, s =~ re

Lemma re_not_empty_correct : forall T (re : reg_exp T),
(exists s, s =~ re) <-> re_not_empty re = true.
Proof.
split; intros. generalize dependent re.
induction re. intros H. destruct H. inversion H.
intros H. destruct H. simpl. auto.
intros H. simpl. auto.
intros H. simpl. apply orb_true_iff. destruct H.
left. apply IHre1.

T : Type
re1, re2 : reg_exp T
IHre1 : (exists s : list T, s =~ re1) -> re_not_empty re1 = true
IHre2 : (exists s : list T, s =~ re2) -> re_not_empty re2 = true
x : list T
H : x =~ App re1 re2

exists s : list T, s =~ re1

subgoal 2 (ID 354) is:
(exists s : list T, s =~ Union re1 re2) -> re_not_empty (Union re1 re2) = true
subgoal 3 (ID 356) is:
(exists s : list T, s =~ Star re) -> re_not_empty (Star re) = true
subgoal 4 (ID 327) is:
exists s : list T, s =~ re