- | cons x l ⇒ match p x with [ true ⇒ nat_return x | false ⇒ aux l ]
- ]
- in
- aux);
-apply
- (program : ∀p:nat → bool.
- ∀l:list nat. ∃res:option nat.
- match res with
- [ None ⇒ ∀y:nat. (mem nat eqb y l = true : Prop) → p y = false
- | Some (x:nat) ⇒ mem nat eqb x l = true ∧ p x = true ]);
-clear program;
- [ cases (aux l1); clear aux;
- simplify in ⊢ (match % in option return ? with [None⇒?|Some⇒?]);
- generalize in match H2; clear H2;
- cases a;
- [ simplify;
- intros 2;
- apply (eqb_elim y n);
- [ intros;
- autobatch
- | intros;
- apply H2;
- simplify in H4;
- exact H4
- ]
- | simplify;
- intros;
- cases H2; clear H2;
- split;
- [ elim (eqb n1 n);
- simplify;
- autobatch
- | assumption
- ]
- ]
- | unfold nat_return; simplify;
- split;
- [ rewrite > eqb_n_n;
- reflexivity
- | assumption
- ]
- | unfold raise_exn; simplify;
- intros;
- change in H1 with (false = true);
- destruct H1
- ]
-qed.
\ No newline at end of file
+ | cons x l ⇒ If p x Then nat_return x Else aux l]
+ in aux
+ :
+ ∀p.∀l.sigma ? (λres.find_spec l p res));
+(* l = x::tl ∧ p x = false *)
+[1: cases (aux l1); clear aux;
+ generalize in match H2; clear H2; cases a; clear a; simplify;
+ [1: intros 2; apply (eqb_elim y n); intros (Eyn); [rewrite > Eyn; assumption]
+ apply H3; simplify in H2; assumption;
+ |2: intros; decompose; repeat split; [2: assumption]; intros;
+ [1: cases (eqb n1 n); simplify; autobatch;
+ |2: generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
+ intro; cases b; clear b; intro Eyn; rewrite > Eyn in H3; simplify in H3;
+ [1: rewrite > (eqb_true_to_eq ? ? Eyn) in H6; rewrite > H1 in H6; destruct H6;
+ |2: lapply H4; try assumption; decompose; clear H4; rewrite > H8;
+ simplify; autobatch depth = 4;]]]
+(* l = x::tl ∧ p x = true *)
+|2: unfold find_spec; unfold nat_return; simplify; repeat split; [2: assumption]
+ [1: rewrite > eqb_n_n; reflexivity
+ |2: intro; generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
+ intro; cases b; clear b; intro Eyn; rewrite > Eyn;
+ [1: rewrite > (eqb_true_to_eq ? ? Eyn);] clear Eyn; simplify; intros;
+ [1: cases H4; reflexivity
+ |2: lapply (mem_x_to_ex_l1_l2 ? ? H2); decompose; rewrite > H6;
+ apply (ex_intro ? ? []); simplify; autobatch;]]
+(* l = [] *)
+|3: unfold raise_exn; simplify; intros; destruct H1;]
+qed.