IndProp: re_not_empty_correct - PullRequest
Новая
       15

IndProp: re_not_empty_correct

1 голос
/ 21 июня 2019 
Lemma re_not_empty_correct : forall T (re : @reg_exp T),
  (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  split.
  - admit. (* I proved it myself *)
  - intros. induction re.
    + simpl in H. discriminate H.
    + exists []. apply MEmpty.
    + exists [t]. apply MChar.
    + simpl in H. rewrite -> andb_true_iff in H. destruct H as [H1 H2].
      apply IHre1 in H1. apply IHre2 in H2.

Вот что мы получили: 

1 subgoal (ID 505)

T : Type
re1, re2 : reg_exp
H1 : exists s : list T, s =~ re1
H2 : exists s : list T, s =~ re2
IHre1 : re_not_empty re1 = true -> exists s : list T, s =~ re1
IHre2 : re_not_empty re2 = true -> exists s : list T, s =~ re2
============================
exists s : list T, s =~ App re1 re2

Теперь мне нужно либо объединить H1 и H2 в exists s : list T, s =~ App re1 re2, либо разбить цель на 2 подзадачи и доказать их отдельно, используя H1 и H2. Но я не знаю, как это сделать.

1 Ответ

1 голос
/ 22 июня 2019

Вы можете думать о exists как о типе пары, который включает значение и его свойство.Как и обычный тип пары, вы можете destruct it.

Например, destruct H1 as [s1 H1]. в этот момент дает 

s1 : list T
H1 : s1 =~ re1

. Учитывая это, подумайте о том, как построить s в цели, которая удовлетворяет s =~ App re1 re2.Затем используйте тактику exists (your answer). (которая изменит цель на (your answer) =~ App re1 re2) и заполните оставшуюся часть доказательства (это должно быть тривиально, если ваш s верен).

...