baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-10-30 12:34:36 +01:00
parent 61c8077d6c
commit c8ec0670f8
1 changed files with 1 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/subsequences.v
View File

@ -314,18 +314,10 @@ Proof.
= map snd (filter fst (combine (repeat false (length u)) u))). = map snd (filter fst (combine (repeat false (length u)) u))).
intro u. induction u. reflexivity. simpl. assumption. apply H0. intro u. induction u. reflexivity. simpl. assumption. apply H0.
exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity. exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
(* deux cas : a = n ou non *) (* deux cas : a = n ou non *)
assert ({a=T} + {a<>T}). apply I. destruct H. assert ({a=T} + {a<>T}). apply I. destruct H.
rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl. rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
rewrite subsequence_cons_eq. split; intro; assumption.
destruct H. destruct H. destruct H.
assert (x0 = nil). symmetry in H. apply length_zero_iff_nil in H.
assumption. rewrite H1 in H0. simpl in H0.