overloaded lemmas in coq (bad) example

OveroadedLemmas.v

(*** oveloaded lemmas *)
(** Lambda World 2018 - How to make ad hoc proof automation less ad hoc
    by Aleksandar Nanevski
    https://www.youtube.com/watch?v=yFIaP1YCcxQ&t=36s *)

Require Import Bool.
Require Import String.
Require Import FunctionalExtensionality.
Require Import List.
Import ListNotations.

Open Scope string_scope.

(*** show *)
Module Show.

Structure Show
  := MkShow {
         sort: Type;
         show: sort -> string;
       }.

Check sort. (* sort: Show -> Type *)
Check show. (* show: forall s: Show, sort s -> string *)

Arguments show {s}.
Check show.
(* show: sort ?s -> string
        where ?s : [ |- Show] *)

Definition show_bool (b: bool): string :=
  if b then "true" else "false".

Canonical Structure Show_bool := MkShow bool show_bool.

Check (show true). (* show true: string *)
Compute (show true). (* = "true" : string *)

Definition show_pair (A B: Show) (p: sort A * sort B): string
  := let (a, b) := p
     in "(" ++ show a ++ ", " ++ show b ++ ")".

Canonical Structure Show_prod (A B: Show)
  := MkShow (sort A * sort B) (show_pair A B).

Check show (true, false). (* show (true, false) : string *)
Compute show (true, false). (* = "(true, false)" : string *)

Fixpoint show_list (X: Show) (xs: list (sort X)): string
  := match xs with
     | nil => "nil"
     | x :: xs => show x ++ " ; " ++ show_list X xs
     end.

Canonical Structure Show_list (X: Show) := MkShow (list (sort X)) (show_list X).

Check show [true; false; false]. (* show [true; false; false] : string *)
Compute show [true; false; false]. (* = "true ; false ; false ; nil" : string *)

Compute show (false, [true; false; false]).
(* = "(false, true ; false ; false ; nil)" : string *)

End Show.

(*** find in set of strings *)
Module Find.

(** functional set of strings *)
Definition sset := string -> bool.
Definition empty: sset := fun _ => false.
Definition add (x: string) (xs: sset): sset
  := fun y => (x =? y) || xs y.

Notation "x ;; xs" := (add x xs) (at level 60, right associativity).

Check "a" ;; "b" ;; empty.
Compute ("a" ;; "b" ;; empty) "a". (* = true : bool *)
Compute ("a" ;; "b" ;; empty) "b". (* = true : bool *)
Compute ("a" ;; "b" ;; empty) "c". (* = false : bool *)

Theorem add_is_in (x: string) (xs: sset): (x ;; xs) x = true.
Proof. unfold add. rewrite eqb_refl. reflexivity. Qed.

Theorem add_comm (x y: string) (s: sset): x ;; y ;; s = y ;; x ;; s.
Proof.
  apply functional_extensionality. intro t.
  unfold add. destruct (x =? t), (y =? t), (s t); reflexivity.
Qed.

Theorem add3_are_in (x y z: string) (s: sset):
  let s' := x ;; y ;; z ;; s
  in s' x && s' y && s' z = true.
Proof.
  simpl. rewrite !andb_true_iff. repeat split.
  - apply add_is_in.
  - rewrite add_comm. apply add_is_in.
  - rewrite (add_comm y z), add_comm. apply add_is_in.
Qed.
  
Structure Find (x: string)
  := MkFind {
         set_of: sset;
         in_set: set_of x = true;
       }.

Check MkFind. (* : forall (x : string) (set_of : sset), set_of x = true -> Find x *)
Check set_of. (* : forall (x : string), Find x -> sset *)
Check in_set. (* : forall (x : string) (f : Find x), set_of x f x = true *)

Arguments in_set {x} {f}.

Canonical Structure Find_hd (x: string) (s: sset)
  := MkFind x (x ;; s) (add_is_in x s).

Check in_set : ("a" ;; empty) "a" = true.

Theorem add_is_in_next (x y: string) (s: sset): s x = true -> (y ;; s) x = true.
Proof.
  intro H. unfold add. rewrite H. apply orb_true_r.
Qed.

Canonical Structure Find_next (x y: string) (f: Find x)
  := let s := set_of x f
     in MkFind x (y ;; s) (add_is_in_next x y s in_set).
(* Find_next is defined *)
(* Warning: Ignoring canonical projection to add by set_of in Find_next: redundant with Find_hd *)
(* [redundant-canonical-projection,records,default] *)

Check in_set : ("a" ;; "b" ;; empty) "b" = true.

Theorem add3_are_in' (x y z: string) (s: sset):
  let s' := x ;; y ;; z ;; s
  in s' x && s' y && s' z = true.
Proof.
  simpl. (* rewrite !in_set. *)
  rewrite !andb_true_iff. repeat split.
  - exact in_set.
  - Fail exact in_set.
    (* Toplevel input, characters 13-19: *)
    (* > exact in_set. *)
    (* >       ^^^^^^ *)
    (* Error: *)
    (* In environment *)
    (* x, y, z : string *)
    (* s : sset *)
    (* The term "in_set" has type "set_of ?x ?f ?x = true" while it is expected to have type *)
    (*  "(x;; y;; z;; s) y = true". *)
Abort.

End Find.