Require Export Setoid.

(* Testare:
   +1. due setoidi con ugualianza diversa sullo stesso tipo
   +2. due setoidi sulla stessa uguaglianza
   +3. due morfismi sulla stessa funzione ma setoidi diversi
   +4. due morfismi sulla stessa funzione e stessi setoidi
   +5. setoid_replace
   +6. solo cammini mal tipati
   +7. esempio (f (g (h E1)))
       dove h:(T1,=1) -> T2, g:T2->(T3,=3), f:(T3,=3)->Prop
   +8. test con occorrenze non lineari del pattern
   +9. test in cui setoid_replace fa direttamente fallback su replace
   10. sezioni
  +11. goal con impl
  +12. testare *veramente* setoid_replace (ora testato solamente il caso
       di fallback su replace)

  Incompatibilita':
    1. full_trivial in setoid_replace
    2. "as ..." per "Add Setoid"
    3. ipotesi permutate in lemma di "Add Morphism"
    4. iff invece di if in "Add Morphism" nel caso di predicati
    5. setoid_replace poteva riscrivere sia c1 in c2 che c2 in c1
       (???? o poteva farlo da destra a sinitra o viceversa? ????)

### Come evitare di dover fare "Require Setoid" prima di usare la
    tattica?

??? scelta: quando ci sono piu' scelte dare un warning oppure fallire?
    difficile quando la tattica e' rewrite ed e' usata in tattiche
    automatiche

??? in test4.v il setoid_rewrite non si puo' sostituire con rewrite
    perche' questo ultimo fallisce per via dell'unificazione

??? ??? <-> non e' sottorelazione di ->. Quindi ora puo' capitare
    di non riuscire a provare goal del tipo A /\ B dove (A, <->) e
    (B, ->) (per esempio)

### Nota: il parsing e pretty printing delle relazioni non e' in synch!
    eq contro (ty,eq). Uniformare

### diminuire la taglia dei proof term

??? il messaggio di errore non e' assolutamente significativo quando
    nessuna marcatura viene trovata

### fare in modo che uscendo da una sezione vengano quantificate le
    relazioni e i morfismi. Hugo: paciugare nel discharge.ml

### implementare relazioni/morfismi quantificati con dei LetIn (che palle...)
    decompose_prod da far diventare simile a un Reduction.dest_arity?
    (ma senza riduzione??? e perche' li' c'e' riduzione?)
    Soluzione da struzzo: fare zeta-conversione.

### fare in modo che impl sia espanso nel lemma di compatibilita' del
    morfismo (richiesta di Marco per poter fare Add Hing)

??? snellire la sintassi omettendo "proved by" come proposto da Marco?  ;-(

### non capisce piu' le riscritture con uguaglianze quantificate (almeno
    nell'esempio di Marco)
### Bas Spitters: poter dichiarare che ogni variabile nel contesto di tipo
    un setoid_function e' un morfismo

### unificare le varie check_...
### sostituire a Use_* una sola eccezione Optimize

  Implementare:
   -2. user-defined subrelations && user-proved subrelations
   -1. trucco di Bruno

  Sorgenti di inefficacia:
    1. scelta del setoide di default per un sostegno: per farlo velocemente
       ci vorrebbe una tabella hash; attualmente viene fatta una ricerca
       lineare sul range della setoid_table

  Vantaggi rispetto alla vecchia tattica:
    1. permette di avere setoidi differenti con lo stesso sostegno,
       ma equivalenza differente
    2. accetta setoidi differenti con lo stesso sostegno e stessa
       equivalenza, scegliendo a caso quello da usare (proof irrelevance)
    3. permette di avere morfismi differenti sulla stessa funzione
       se hanno dominio o codominio differenti
    4. accetta di avere morfismi differenti sulla stessa funzione e con
       lo stesso dominio e codominio, scegliendo a caso quello da usare
       (proof irrelevance)
    5. quando un morfismo viene definito, se la scelta del dominio o del
       codominio e' ambigua l'utente puo' esplicitamente disambiguare
       la scelta fornendo esplicitamente il "tipo" del morfismo
    6. permette di gestire riscritture ove ad almeno una funzione venga
       associato piu' di un morfismo. Vengono automaticamente calcolate
       le scelte globali che rispettano il tipaggio.
    7. se esistono piu' scelte globali che rispettano le regole di tipaggio
       l'utente puo' esplicitamente disambiguare la scelta globale fornendo
       esplicitamente la scelta delle side conditions generate.
    8. nel caso in cui la setoid_replace sia stata invocata al posto
       della replace la setoid_replace invoca direttamente la replace.
       Stessa cosa per la setoid_rewrite.
    9. permette di gestire termini in cui il prefisso iniziale dell'albero
       (fino a trovare il termine da riscrivere) non sia formato esclusivamente
       da morfismi il cui dominio e codominio sia un setoide.
       Ovvero ammette anche morfismi il cui dominio e/o codominio sia
       l'uguaglianza di Leibniz. (Se entrambi sono uguaglianze di Leibniz
       allora il setoide e' una semplice funzione).
   10. [setoid_]rewrite ... in ...
       setoid_replace ... in ...
       [setoid_]reflexivity
       [setoid_]transitivity ...
       [setoid_]symmetry
       [setoid_]symmetry in ...
   11. permette di dichiarare dei setoidi/relazioni/morfismi in un module
       type
   12. relazioni, morfismi e setoidi quantificati
*)

Axiom S1: Set.
Axiom eqS1: S1 -> S1 -> Prop.
Axiom SetoidS1 : Setoid_Theory S1 eqS1.
Add Setoid S1 eqS1 SetoidS1 as S1setoid.

#[export] Instance eqS1_default : DefaultRelation eqS1 := {}.

Axiom eqS1': S1 -> S1 -> Prop.
Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'.
Add Setoid S1 eqS1' SetoidS1' as S1setoid'.
Add Setoid S1 eqS1' SetoidS1'_bis as S1setoid''.

Axiom S2: Set.
Axiom eqS2: S2 -> S2 -> Prop.
Axiom SetoidS2 : Setoid_Theory S2 eqS2.
Add Setoid S2 eqS2 SetoidS2 as S2setoid.

Axiom f : S1 -> nat -> S2.
Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat. Admitted.
Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat2. Admitted.

Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
 intros.
 rewrite H.
 reflexivity.
Qed.

Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
 intros.
 setoid_replace x with y.
 reflexivity.
 assumption.
Qed.

Axiom g : S1 -> S2 -> nat.
Add Morphism g with signature (eqS1 ==> eqS2 ==> eq) as g_compat. Admitted.

Axiom P : nat -> Prop.
Theorem test2:
 forall x x' y y', (eqS1 x x') -> (eqS2 y y') -> (P (g x' y')) -> (P (g x y)).
 intros.
 rewrite H.
 rewrite H0.
 assumption.
Qed.

Theorem test3:
 forall x x' y y',
  (eqS1 x x') -> (eqS2 y y') -> (P (S (g x' y'))) -> (P (S (g x y))).
 intros.
 rewrite H.
 rewrite H0.
 assumption.
Qed.

Theorem test4:
 forall x x' y y', (eqS1 x x') -> (eqS2 y y') -> (S (g x y)) = (S (g x' y')).
 intros.
 rewrite H.
 rewrite H0.
 reflexivity.
Qed.

Theorem test5:
 forall x x' y y', (eqS1 x x') -> (eqS2 y y') -> (S (g x y)) = (S (g x' y')).
 intros.
 setoid_replace (g x y) with (g x' y').
 reflexivity.
 rewrite <- H0.
 rewrite H.
 reflexivity.
Qed.

Axiom f_test6 : S2 -> Prop.
Add Morphism f_test6 with signature (eqS2 ==> iff) as f_test6_compat. Admitted.

Axiom g_test6 : bool -> S2.
Add Morphism g_test6 with signature (eq ==> eqS2) as g_test6_compat. Admitted.

Axiom h_test6 : S1 -> bool.
Add Morphism h_test6 with signature (eqS1 ==> eq) as h_test6_compat. Admitted.

Theorem test6:
 forall E1 E2, (eqS1 E1 E2) -> (f_test6 (g_test6 (h_test6 E2))) ->
  (f_test6 (g_test6 (h_test6 E1))).
 intros.
 rewrite  H.
 assumption.
Qed.

Theorem test7:
 forall E1 E2 y y', (eqS1 E1 E2) -> (eqS2 y y') ->
  (f_test6 (g_test6 (h_test6 E2))) ->
   (f_test6 (g_test6 (h_test6 E1))) /\ (S (g E1 y')) = (S (g E2 y')).
  intros.
  rewrite H.
  split; [assumption | reflexivity].
Qed.

Axiom S1_test8: Set.
Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.

#[export] Instance eqS1_test8_default : DefaultRelation eqS1_test8 := {}.

Axiom f_test8 : S2 -> S1_test8.
Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted.

Axiom eqS1_test8': S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8' : Setoid_Theory S1_test8 eqS1_test8'.
Add Setoid S1_test8 eqS1_test8' SetoidS1_test8' as S1_test8setoid'.

(*CSC: for test8 to be significant I want to choose the setoid
  (S1_test8, eqS1_test8'). However this does not happen and
  there is still no syntax for it ;-( *)
Axiom g_test8 : S1_test8 -> S2.
Add Morphism g_test8 with signature (eqS1_test8 ==> eqS2) as g_compat_test8. Admitted.

Theorem test8:
 forall x x': S2, (eqS2 x x') ->
  (eqS2 (g_test8 (f_test8 x)) (g_test8 (f_test8 x'))).
  intros.
  rewrite H.
Abort.

(*Print Setoids.*)