commit before putting void and epsilon in pat

src/Sorting.v

@@ -238,6 +238,8 @@ Definition derive (s:mysort) (p:term)
 
 
 
+(* Theorem der_in_derive : der x e \in derive s p. *)
+
 
 Fixpoint check_pattern_term (p:term) (l:list mysort) : bool := 
   match l with 
@@ -274,16 +276,30 @@ Fixpoint check_pattern_term_faster (p:term) (l:list mysort) : bool :=
     end
   end. 
 
+Lemma fold_left_id {bo te:Type} : forall l:list te, forall t f f', f = f' -> @fold_left bo te f l t = fold_left f' l t.
+intros. subst f. reflexivity. Qed.
 
 Lemma check_pattern_term_faster_eq_check_pattern_term (p:term) (l:list mysort) :
   check_pattern_term_faster p l = check_pattern_term p l.
   Proof.
+    unfold check_pattern_term, check_pattern_term_faster.
+    auto. 
     induction l.
     - auto.
-    - destruct p as [fp op]. simpl.
+    - auto. destruct p as [fp op]. simpl.
     destruct fp.
-    + unfold derive,derive_func. simpl.
-     (* unfold fold_left. auto. rewrite IHl. simpl. auto. *)
+    + apply fold_left_id.
+    apply functional_extensionality.
+    intros bo.
+    apply functional_extensionality.
+    intros te.
+    destruct bo eqn:BI.
+    ++ rewrite (Bool.orb_true_r (check_pattern_term te l)).
+    rewrite (Bool.orb_true_r).
+    reflexivity.
+    ++ Search (orb _ false).
+    rewrite (Bool.orb_false_r).
+    rewrite (Bool.orb_false_r).
     Abort.
 
 (* Fixpoint check_pattern_term_in_dec (p:term) (l:list mysort) : bool :=