-unification hint 0 ≔ S,a,b;
- R ≟ LIST S
-(* -------------------------------------------- *) ⊢
- eq_list S a b ≡ eq_rel (list S) (eq0 R) a b.
-
-notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
-notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
-notation "B ⇒\sub 0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
-notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
-
-interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
-interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
-
-ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
-
-nlemma exists_is_morph: (* BUG *) ∀S,T:setoid.∀P: S ⇒_1 (T ⇒_1 (CProp[0]:?)).
- ∀y,z:S.y =_0 z → (Ex T (P y)) = (Ex T (P z)).
-#S T P y z E; @;
-##[ *; #x Px; @x; alias symbol "refl" (instance 4) = "refl".
- alias symbol "prop2" (instance 2) = "prop21".
- napply (. E^-1‡#); napply Px;
-##| *; #x Px; @x; napply (. E‡#); napply Px;##]
-nqed.
-
-ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? P); ##| #P1 P2 E; @;
-*; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
-nqed.
-
-nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
- ∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
-#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
-
-(* desiderata : Σ(λx.H‡#)
- ottenute : Σ H (λx,H.H‡#) -- quindi monoriscrittura. H toplevel permette inferenza di y e z in Sig
-*)
-
-nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)).
-#S m x y E;
-
-napply (trans1 ????? (Sig ????? E (λw,H.
- (prop11 ?(unary_morphism1_setoid1 ??)???
- (prop11 ?(unary_morphism1_setoid1 ??)???
- H
- ?? (refl ???))
- ?? (refl1 ???))))).
-napply refl1.
-nqed.
-
-nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:setoid1_of_setoid S.x =_1 y →
- (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
-#S m x y E;
-napply (trans1 ?????
-(#‡
- (Sig ????? E (λw,H.
- (prop11 ?(unary_morphism1_setoid1 ??)???
- (prop11 ?(unary_morphism1_setoid1 ??)???
- H
- ?? (refl ???))
- ?? (refl1 ???)))))).
-napply refl1.
-
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "refl" (instance 5) = "refl".
-alias symbol "prop2" (instance 3) = "prop21".
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-(* super bug 1+1:
- eseguire senza modificare per ottenrere degli alias, fare back di 1 passo
- e ri-eseguire. Se riesegue senza aggiungere altri alias allora hai gli
- alias giusti (ma se fate back di più passi, gli alias non vanno più bene...).
- ora (m x w) e True possono essere sostituiti da ?, se invece
- si toglie anche l'∧, allora un super bug si scatena (meta contesto locale
- scazzato, con y al posto di x, unificata con se stessa ma col contesto
- locale corretto...). lo stesso (o simile) bug salta fuori se esegui
- senza gli alias giusti con ? al posto di True o (m x w).
-
- bug a parte, pare inferisca tutto lui...
- la E astratta nella prova è solo per fargli inferire x e y, se Sig
- lo si riformula in modo più naturale (senza y=z) allora bisogna passare
- x e y esplicitamente. *)
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-(*napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); *)
-
-(* OK *)
-napply (.= (Sig ? ? (?) ?? E (λw,H.
- (prop11 ?(unary_morphism1_setoid1 ??)???
- (prop11 ?(unary_morphism1_setoid1 ??)???
- H
- ?? (refl ???))
- ?? (refl1 ???))))).
-napply refl1.
-
- (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ????
- (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ????
- H
- (refl ??))
- (refl ? True))))).
-
-prop11 ???????? (prop11 ???????? H (refl ??)) (refl ??))));
-
-napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#)));
-
-
-napply (.= (Sig ? S (λw,x.?) ?? E (λw,H.(H‡#)‡#)));
-(Ex S (λx.?P x y)) ==?==
-//; nqed.
-STOP
-napply (λw:S.(.= ((E‡#)‡#)) #); ##[##2: napply w| napply m. #H; napply H;
-
-
-
- let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
- form x = form y.
- #S ee x y E;
- nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
-
- nnormalize;
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
-
- ncheck (exists_is_morph (LIST S) (LIST S) ? ?? (E‡#)).
- nletin xxx ≝ (exists_is_morph); (LIST S)); (LIST S) ee x y E);
-
- nchange with (F x = F y);
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
- napply (.= † E);
- napply #.