Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sat, Feb 10, 2018 at 09:33:15AM -0500, Mitchell Wand wrote:
> ​Can anybody tell me where to find the solutions to "An introduction to
> small scale reflection​ in Coq"?
> 
> The paper promises solutions at
> www.msr-inria.inria.fr/Projects/math-components, but I couldn't find them.

Dear Mitch, I found the solutions (in attachment).

I would also like to point out that, if you are looking for an
introduction to ssr/math-comp you may also want to take a look at
the book draft: https://math-comp.github.io/mcb/

Best
-- 
Enrico Tassi
(******************************************************************************)
(* Solutions of exercises : A script language for structured proofs           
*)
(******************************************************************************)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import paths choice fintype tuple finset.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.


(******************************************************************************)
(* Exercise 3.1.1                                                             
*)
(******************************************************************************)

Section Tauto.

Variables A B C : Prop.

(* The exact tactic takes its argument on top of the goal stack *)
Lemma tauto1 : A -> A.
Proof.
exact.
Qed.

(* exact: hAB behaves like (by apply: hAB) and hence finds the hypothesis A
in the context needed to solve the goal *)
Lemma tauto2 : (A -> B) -> (B -> C) -> A -> C.
Proof.
move=> hAB hBC hA.
apply: hBC.
exact: hAB.
Qed.

Lemma tauto4 : A /\ B <-> B /\ A.
Proof. by split; case=> h1 h2; split. Qed.
  
End Tauto.

(******************************************************************************)
(* Exercise 3.1.2                                                             
*)
(******************************************************************************)

Section MoreBasics.

Variables A B C : Prop.
Variable P : nat -> Prop.

Lemma foo1 : ~(exists x, P x) -> forall x, ~P x.
move=> h x Px.
apply: h.
by exists x.
Qed.


Lemma foo2 : (exists x, A -> P x) -> (forall x, ~P x) -> ~A.
Proof.
case=> x hx hP hA.
apply: (hP x).
exact: hx.
Qed.
End MoreBasics.

(******************************************************************************)
(* Exercise 3.1.3                                                             
*)
(******************************************************************************)

(* Try Search "<=" to see the various notations featuring <= *)

(* The first line of the returned answer gives the name of
   the predicate (leq) *)
Search "_ <= _".

(* The Print command shows that leq is defined using subtraction *)
Print leq.

(* This time we see that the first line of the answer gives the *)
(*answer: there is no constant defining "<" but the notation hides a *)
(* defintiion using leq *)

Search "_ < _".

(* Both cases gereated by the induction lead to trivial goals *)
Lemma tuto_subnn : forall n : nat, n - n = 0.
Proof. by elim=> [|n ihn]. Qed.
  
(* This proof is an induction on m, followed by a case  analysis on *)
(* the second n. Base case is trivial (hence discarded by the // *)
(* switch. *)
Lemma tuto_subn_gt0 : forall m n, (0 < n - m) = (m < n).
Proof. elim=> [|m IHm] [|n] //; exact: IHm. Qed.


(* This proof starts the same way as the one of subn_gt0. *)
(* Then two rewriting are chained to reach to trivial subgoals *)
Lemma tuto_subnKC : forall m n : nat, m <= n -> m + (n - m) = n.
Proof.
elim=> [|m IHm] [|n] // Hmn.
Search _ (_.+1 + _ = _.+1).
by rewrite addSn IHm.
Qed.
  
(* The first Search command suggests we need to use something like *)
(*subn_add2r, hence to transform n into n - p + p *)
(* The second Search command finds the appropriate lemma. We rewrite *)
(*it from right to left, only at the second occurrence of n, the *)
(*condition of the lemma is fullfilled thanks to the le_pn hypothesis, *)
(*hence the generated subgoal is closed by the // switch *)

Lemma tuto_subn_subA : forall m n p, p <= n -> m - (n - p) = m + p - n.
Proof. 
move=> m n p le_pn.
Search _ (_ + _ - _ = _) in ssrnat.
Search _ (_ - _ + _).
rewrite -{2}(subnK le_pn) // subn_add2r.
done. 
Qed.

(******************************************************************************)
(* Exercise 3.5.1                                                             
*)
(******************************************************************************)

(* The Check instruction only gives the type of a constant, the *)
(*statement of a lemma. The Print command gives the body of the *)
(*definition, and possibly some extra information (scope, implicit *)
(*arguments,...). Print should not be used in general on lemmas *)
(* since the body of a proof is seldom relevant...*)

Print edivn.
Print edivn_rec.
Print edivn_spec.
(* The edivn_spec is defined as a CoInductive predicate. The intended *)
(* meaning is not to define an coinductive structure, but rather an *)
(* inductive one. CoInductive in this case indeed behaves as Inductive *)
(*but does not generate an induction principle, which would be is *)
(*useless in this case. *)


(******************************************************************************)
(* Exercise 3.5.2                                                             
*)
(******************************************************************************)

(* At this point, the top of the goal stack was featuring three *)
(*natural numers: an induction on the first one generated two subgoals. *)
(*In the second subgoal, corresponding to the inductive case, the *)
(*generated natural number and induction hypothesis have  been *)
(*introduced by the branching intro pattern [| n IHn], which leaves *)
(*the first subgoal, corresponding to the base case of the induction, *)
(*unchanged. Then [|m] performs in both subgoals a case analysis on the *)
(*second natural number. This case analysis again leads to two new *)
(*subgoal for each initial branch (which makes four subgoals). In the *)
(*second case of the analysis, the new natural number is introduced *)
(*and named m. Then the third natural number is uniformly introdued in *)
(*the four cases under the name q. Finally the //= switch simplifies *)
(*in the four bracnhes and closes the goals that have become trivial *)
(*(i.e. which are solved by done). *)

(******************************************************************************)
(* Exercise 3.5.3                                                             
*)
(******************************************************************************)

(* The pattern [// | le_dm] closes the first subgoal and introduces an *)
(*hypothesis named le_dm in the second subgoal. This is equivalent to *)
(* // le_dm. *)

(******************************************************************************)
(* Exercise 3.5.4                                                             
*)
(******************************************************************************)

(* Replacing (ltnP m d) by ltnP does not change the behaviour of the *)
(*script: Coq's unification is powerful enough to guess the arguments *)
(*in this case since there is only one instance of the comparison in *)
(* (_ <_) the goal. Arguments are mandatory only in the case the frist *)
(*occurrence of the comparison is not the one the user whould like to *)
(*pick as support for ase analysis. *)

Check ltnP.
Print ltn_xor_geq.

(* For any two natural numbers n and m, (ltn_xor_geq m n) is a binary *)
(*relation on boolean. Its inductive definition has two constructors *)
(*and states that *)
(* - (false, true) is in the relation(ltn_xor_geq m n) as soon as 
     m < n *)
(* - (true, false) is in the relation(ltn_xor_geq m n) as soon as 
     n <= m *)
(* The inductive construction implies that these two rules are the *)
(*only ways to populate the relation.*)
(* Now the theorem:*)
(* ltnP :  forall m n : nat, ltn_xor_geq m n (n <= m)(m < n)*)
(*proves that for any two natural numbers m and n, there are only two*)
(*possible situations:*)
(* - either m < n (first rule of the relation definition), and in this *)
(*case n <= m = false and m < n = true *)
(* - or n <= m (second rule of the relation definition, and in this *)
(*case n <= m = true and m < n = false *)
(* A case analysis on this result hence generates two subgoals, one *)
(*for each constructor of ltn_xor_gep. In each subgoal the hypothesis *)
(*of the rule (repectively m < n and n <= m) appears on the stack. Also *)
(*every occurrence of (n <= m) and (m < n) is replaced by the value *)
(*imposed by the ltn_xor_gep constructor used in the branch.*)

CoInductive tuto_compare_nat (m n : nat) : bool -> bool -> bool -> Set :=
  | TCompareNatLt of m < n : tuto_compare_nat m n true false false
  | TCompareNatGt of m > n : tuto_compare_nat m n false true false
  | TCompareNatEq of m = n : tuto_compare_nat m n false false true.

(* Let's check against what is defined in the ssrnat library *)
Print compare_nat.

Lemma tuto_ltngtP : forall m n, compare_nat m n (m < n) (n < m) (m == n).
Proof.
move=> m n; rewrite ltn_neqAle eqn_leq; case: ltnP; first by constructor.
by rewrite leq_eqVlt orbC; case: leqP => Hm; first move/eqnP; constructor.
Qed.




(******************************************************************************)
(* Solutions of exercises : Small scale reflection, first examples            
*)
(******************************************************************************)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import paths choice fintype tuple finset.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.


(******************************************************************************)
(* Exercise 4.1.1                                                             
*)
(******************************************************************************)

(* The proof goes by case analysis on the truth table, applying the *)
(*appropriate constructor of the reflect predicate in every meaningful *)
(*case. The other case ask a proof of False in a conctext where False *)
(*can be obtained as a hypothesis after destructing a conjunction (the *)
(*last case tactic) *)

Lemma tuto_andP : forall b1 b2 : bool, reflect (b1 /\ b2) (b1 && b2).
Proof. by case; case; constructor; auto; case. Qed.

(* Again this lemma is a macro for a cacse analysis on the truth table *)
(*of b1 b2 and (b1 || b2) *)

Lemma tuto_orP : forall b1 b2 : bool, reflect (b1 \/ b2) (b1 || b2).
Proof. by case; case; constructor; auto; case. Qed.

(******************************************************************************)
(* Exercise 4.1.2                                                             
*)
(******************************************************************************)

(* The first solution follows the hint given in the tutorial. In fact *)
(* it is sufficient to perform case analysis on the constructor of the *)
(*reflect hypothesis as done in the second solution. *)
Lemma tuto_iffP : forall (P Q : Prop) (b : bool),
      reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.
Proof. by move=> P Q; case; case; constructor; auto. Qed.


Lemma alternate_tuto_iffP : forall (P Q : Prop) (b : bool),
      reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.
Proof. by move=> P Q b; case; constructor; auto. Qed.

(******************************************************************************)
(* Exercise 4.2.1                                                             
*)
(******************************************************************************)

(*We use a section to factorize the type of elements in the *)
(*sequences*)

Section Exo_4_2_1.

Variable A : Type.

(* We use implicit type annotations to avoid casting quantified *)
(*variables : *)
Implicit Types s : seq A.
Implicit Types x : A.

(* The type of x has been declared implicit, hence the type of s1 and *)
(*s2 and inferred: *)
Fixpoint tuto_cat s1 s2 :=
match s1 with
  |[::] => s2
  | x :: s' => x :: (tuto_cat s' s2)
end.

(* Using the ssreflect pattern conditional this code can be shrinked *)
(*into the actual program present in the seq library:*)
Fixpoint alternate_tuto s1 s2 :=
  if s1 is x :: s' then x :: (tuto_cat s' s2) else s2.


(* The proof goes by induction on the first list. We do not need to be *)
(*general with respect to the second list, hence we introduce it *)
(*before the induction. The first case is solved on the fly by the //= *)
(*simple+solve switch, and x and s1 are introduced in the remaining *)
(*goal. The last hypothesis is directly rewritten without being *)
(*introduced, generating an equality between convertible terms. This *)
(*equality being trivial it is solved by the prenex 'by' tactic *)
Lemma tuto_size_cat : forall s1 s2,
   size (s1 ++ s2) = size s1 + size s2.
Proof. by move=> s1 s2; elim: s1 => //= x s1 ->. Qed.

(* We use again a pattern conditional *)
Fixpoint tuto_last (A : Type)(x : A)(s : seq A) {struct s} := 
  if s is x' :: s' then tuto_last x' s' else x.

(* Again an induction on the first list *)
Lemma tuto_last_cat : forall x s1 s2,
  last x (s1 ++ s2) = last (last x s1) s2.
Proof. by move=> x s1 s2; elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.

Fixpoint tuto_take n s {struct s} :=
  match s, n with
  | x :: s', n'.+1 => x :: take n' s'
  | _, _ => [::]
  end.


(* Here we have two options: a recursion on the nat or on the seq.*)
(* Decreazing on the seq has better compositional properties: it *)
(*allows more fixpoints further defined to decrease structurally *)
Fixpoint tuto_drop n s {struct s} :=
  match s, n with
  | _ :: s', n'.+1 => drop n' s'
  | _, _ => s
  end.

Definition tuto_rot n s := drop n s ++ take n s.

Lemma tuto_rot_addn : forall m n s, m + n <= size s ->
  rot (m + n) s = rot m (rot n s).
Proof.
(* We first transform the inequality hypothesis into a case *)
(*disjunction between equality or strict inequality. *)
move=> m n s; rewrite leq_eqVlt. 
(* Then a view allows to proceed to the case analysis by generating *)
(* two goals *)
case/predU1P=> [Emn|Hmn].
(*  1st case: equality. We rewrite the hypothesis, then the rot_size *)
(*lemma (try to guess the name of the lemma according to the ssr *)
(*discipline, or use the Search command, for instance:
Search _ rot size.*)
rewrite Emn rot_size.
(* Again, use the Search command:*)
Search _ (rot _ (rot _ _) = _).
  rewrite rot_add_mod -Emn ?leq_addr ?leq_addl //.
  by rewrite  Emn leqnn rot_size.
(* a more elegant proof of this last step would be:
  by rewrite  -{1}(rotrK m s) /rotr -Emn addKn.
  It is worth also browsing the source of the library to discover new
  functions that could help you, like rotr is this case *)
(* Remember rot is programmed from cat take and drop:
Search _ cat take drop.*)
rewrite -{1}(cat_take_drop n s) /rot !take_cat !drop_cat.
Search _ (size (take _ _) = _).
have Hns : n <= size s by apply: leq_trans (leq_addl _ _) (ltnW Hmn).
rewrite !(size_takel Hns).
(* We directly rewrite the condition proved forward *)
have -> : m + n < n = false by rewrite ltnNge leq_addl.  
rewrite size_drop.
have -> :  m < size s - n by rewrite ltnNge leq_sub_add -ltnNge addnC.
by rewrite addnK catA.
Qed.

(* Look at the source of the seq.v file for a shorter proof! *)

End Exo_4_2_1.
(******************************************************************************)
(* Exercise 4.2.2                                                             
*)
(******************************************************************************)

Section Exo_4_2_2.

Variable A : Type.

(* We use implicit type annotations to avoid casting quantified *)
(*variables : *)
Implicit Types s : seq A.
Implicit Types x : A.

(* We fix an arbitrary predicate a *)
Variable a : pred A.

(* We use again a pattern conditional *)
Fixpoint tuto_count s := if s is x :: s' then a x + tuto_count s' else 0.

Lemma tuto_count_predUI : forall a1 a2 s,
 count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
Proof.
move=> a1 a2. 
(* The proof goes by induction on the list. In the inductive case, we *)
(*introduce the head, the tail, and the induction hypothesis. After
 simplification, the case case is trivial, and since simplification is
 also usefull in the inductive case, the //= swith both simplifies and
 closes the first goal.*)
elim=> [|x s IHs] //=. 
(* Now a couple of arithmetic rewriting before using the inductive 
hypothesis*)
rewrite addnCA -addnA  addnA addnC IHs -!addnA.
(* The nat_congr tactic (and Ltac tactic defined in ssrnat) normalizes *)
(*both sides of a nat equality to be able to use some congruence, here *)
(*with count a1 s + _ *)
nat_congr.
(* We use it a second time to eliminate (count a2 s) *)
nat_congr.
(* Now it is only a matter of truth table *)
by case (a1 x); case (a2 x).
Qed.

(* After closing the section, tuto_count_filter has the type required *)
(* by the exercise *)
Lemma tuto_count_filter : forall s, count a s = size (filter a s).
Proof. by elim=> [|x s IHs] //=; rewrite IHs; case (a x). Qed.

End Exo_4_2_2.

(******************************************************************************)
(* Exercise 4.3.1                                                             
*)
(******************************************************************************)

Section Exo_4_3_1.

(* We fix an arbitrary eqType T *)
Variable T : eqType.

(* We use implicit type annotations to avoid casting quantified *)
(*variables *)
Implicit Types x y : T.
Implicit Type b : bool.

Lemma tuto_eqxx : forall x, x == x.
Proof. by move=> x; apply/eqP. Qed.

(* First solution *)
Lemma tuto_predU1l : forall x y b, x = y -> (x == y) || b.
Proof. by move=> x y b exy; rewrite exy eqxx. Qed.

(* Second solution. The syntax move/eqP-> is equivalent to *)
(*move/eqP => ->, i.e. it applies the view to the top element of the *)
(*goal stack and rewrites the term obtains immediatly without *)
(*introducing it in the context. Similarily, move-> is equaivalent to *)
(*move=> -> and rewrite the top element of the goal (which should be *)
(*an equality) in the rest of the goal, without introducing it in the context 
*)

Lemma tuto_predU1l_alt_proof : forall x y b, x = y -> (x == y) || b.
Proof. by move=> x y b; move/eqP->. Qed.

(* The proof script is the same in both branches thanks to the *)
(* symmetry of the view mechanism. Remeber the 'by' tactical contains *)
(* the 'split' tactic and hence solves the goal after the last *)
(* assumption interpretation move/eqP. *)
Lemma tuto_predD1P : forall x y b, reflect (x <> y /\ b) ((x != y) && b).
Proof.
by move=> x y b; apply: (iffP andP) => [] []; move/eqP.
Qed.

(* Remember that _ != _ denotes the boolean disequality *)
(* Coq's unification is able to infer from the goal the arguments to *)
(* provide to the eqP lemma*)
Lemma tuto_eqVneq : forall x y, {x = y} + {x != y}.
Proof. by move=> x y; case: eqP; [left | right]. Qed.

End Exo_4_3_1.(******************************************************************************)
(* Solutions of exercises : Type inference by canonical structures            
*)
(******************************************************************************)


Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq paths.
Require Import choice fintype  tuple finset.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(******************************************************************************)
(* Exercise 5.1.1                                                             
*)
(******************************************************************************)

Record zmodule_mixin (T : Type) : Type := ZmoduleMixin {
  zero : T;
  opp : T -> T;
  add : T -> T -> T;
  addA : associative add;
  addC: commutative add;
  addm0 : left_id zero add;
  add0m : left_inverse zero opp add
}.

Record zmodule : Type := Zmodule {
  carrier :> Type;
  spec : zmodule_mixin carrier
}.


Definition bool_zmoduleMixin := ZmoduleMixin addbA addbC addFb addbb.


Definition bool_zmodule := Zmodule bool_zmoduleMixin.


Definition zmadd (Z : zmodule) := add (spec Z).

Notation "x \+ y" :=    (@zmadd _ x y)(at level 50,left associativity).


(* We first need to prove that zmadd is associative and commutative *)
(* The proof consists in breaking successivly the two nested records *)
(*to recover all the ingredients present in the zmodule_mixin. Then *)
(*the goal becomes trivial because the associative and commutative *)
(*requirements were present in the spec. *)
Lemma zmaddA : forall m : zmodule, associative (@zmadd m).
Proof. by case=> Mc []. Qed.

Lemma zmaddC : forall m : zmodule, commutative (@zmadd m).
Proof. by case=> Mc []. Qed.

(* No we can conveniently prove the lemma *)
(* The ssreflect rewrite tactic allows rewrite redex selection by *)
(* pattern, and this is used here to select the occurrence where *)
(* commutativity should be used.*)
Lemma zmaddAC : forall (m : zmodule)(x y z : m), x \+ y \+ z = x \+ z \+ y.
Proof.
by move=> M x y z; rewrite -zmaddA [y \+ _]zmaddC zmaddA.
Qed.

(******************************************************************************)
(* Exercise 5.2.1                                                             
*)
(******************************************************************************)

(* Be aware that the Print command shows terms as they are represented *)
(*by the system, which is possibliy syntactically slightly different *)
(*from the definition typed by the user (specially in the case of *)
(*nested pattern matching *)
Print nat_eqType.
Print nat_eqMixin.
Print eqn.
Check @eqnP.

Print bool_eqType.
Print bool_eqMixin.
Print eqb.
Check @eqbP.

(* Look for nat, bool, Equality.sort in the answer of the command: *)
Print Canonical Projections.
(* The equations stored after these declarations are respectively :
[ Equality.sort ? == nat  ] => ? = nat_eqType
[ Equality.sort ? == bool ] => ? = bool_eqType
*)


(******************************************************************************)
(* Exercise 5.2.2                                                             
*)
(******************************************************************************)

(* This script uses a complex intro pattern: the apply: (iffP andP) *)
(*tactic breaks the reflect goal into two subgoals for each *)
(*implication, while interpreting the first assumption of each *)
(*generated sugoal with the andP view. Then the [[] | [<- <- ]] // *)
(*intropattern simultaneously describes the introduction operations *)
(*performed on the two subgoals:*)
(*- on the first subgoal the [] casing intropattern splits the *)
(*conjunction hypothesis into two distinct assumptions.*)
(*   - on the second hypothesis the  [<- <- ] is composed of a [] *)
(*casing intropattern and two <- rewrite intropatterns. [] performs an *)
(*injection on the equality, generating two equalities, one for each *)
(*components of the pairs.  Then both equalities are rewritten form *)
(*left to right by <- <-.  This subgoal is now trivial hence closed by *)
(*// *)
Lemma tuto_pair_eqP : forall T1 T2, Equality.axiom (pair_eq T1 T2).
Proof. 
move=> T1 T2 [u1 u2] [v1 v2] /=. 
apply: (iffP andP) => [[]|[<- <-]] //.
by do 2!move/eqP->.
Qed.


(******************************************************************************)
(* Exercise 5.3.1                                                             
*)
(******************************************************************************)
Section SeqMem.

Variable T : eqType.

Implicit Type s : seq T.
Implicit Types x y : T.

Lemma tuto_in_cons : forall y s x,
  (x \in y :: s) = (x == y) || (x \in s).
Proof. by []. Qed.

(* by [] is an alternative syntax for the done tactic *)
Lemma tuto_in_nil : forall x, (x \in [::]) = false.
Proof. by []. Qed.

Lemma tuto_mem_seq1 : forall x y, (x \in [:: y]) = (x == y).
Proof. by move=> x y; rewrite in_cons orbF. Qed.

(* Here we do not even need to name the elements introduced since they *)
(*will never be used later in the script. We let the system choose *)
(*names using the move=> * tactic. *)
Lemma tuto_mem_head : forall x s, x \in x :: s.
Proof.  by move=> *; exact: predU1l. Qed.

(******************************************************************************)
(* Exercise 5.3.2                                                             
*)
(******************************************************************************)

Lemma tuto_mem_cat : forall x s1 s2,
  (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
Proof.
by move=> x s1 s2; elim: s1 => //= y s1 IHs; rewrite !inE /= -orbA -IHs.
Qed.

Lemma tuto_mem_behead: forall s, {subset behead s <= s}.
Proof. move=> [|y s] x //; exact: predU1r. Qed.

Fixpoint tuto_has (a : pred T) s := 
  if s is x :: s' then a x || tuto_has a s' else false.

Lemma tuto_hasP : forall (a : pred T) s,
  reflect (exists2 x, x \in s & a x) (has a s).
Proof.
move=> a; elim=> [|y s IHs] /=; first by right; case.
case ay: (a y); first by left; exists y; rewrite ?mem_head.
apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead.
Search _ (_ \in cons _ _).
by move: ysx ax; rewrite in_cons; case/orP=> //; move/eqP->; rewrite ay.
Qed.

(* In fact, the last line of the previous script can be simplified by *)
(*the use of the predU1P view lemma. This is possible since the mem *)
(*function on sequences is exactly programmed as required by the statement *)
(*of predU1P. *)


Lemma tuto_hasP_alt: forall (a : pred T) s,
  reflect (exists2 x, x \in s & a x) (has a s).
Proof.
move=> a; elim=> [|y s IHs] /=; first by right; case.
case ay: (a y); first by left; exists y; rewrite ?mem_head.
apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead.
by case: (predU1P ysx) ax => [->|//]; rewrite ay.
Qed.


Fixpoint tuto_all a s := if s is x :: s' then a x && tuto_all a s' else true.

(* We again use predU1P to shortcut the combination of incons and eqP *)
Lemma tuto_allP : forall (a : pred T) s,
    reflect (forall x, x \in s -> a x) (all a s).
Proof.
Proof.
move=> a; elim=> [|x s IHs]; first by left.
rewrite /= andbC; case: IHs => IHs /=.
  apply: (iffP idP) => [Hx y|]; last by apply; exact: mem_head.
  by case/predU1P=> [->|Hy]; auto.
by right; move=> H; case IHs; move=> y Hy; apply H; exact: mem_behead.
Qed.

End SeqMem.