Skip to content

Commit

Permalink
make sure No uses HIT idiom
Browse files Browse the repository at this point in the history 
Signed-off-by: Ali Caglayan <[email protected]>
  • Loading branch information
@Alizter
Alizter committed Oct 7, 2023
1 parent 9e78703 commit 198772b
Show file tree
Hide file tree
Showing 2 changed files with 166 additions and 0 deletions.
164 changes: 164 additions & 0 deletions test/bugs/github1759.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,164 @@
Require Import Basics Types.

Check failure on line 1 in test/bugs/github1759.v

View workflow job for this annotation

GitHub Actions / opam-build (supported, ubuntu-latest) 

Cannot find a physical path bound to logical path Types.

Check failure on line 1 in test/bugs/github1759.v

View workflow job for this annotation

GitHub Actions / opam-build (8.17, ubuntu-latest) 

Cannot find a physical path bound to logical path Types.

Check failure on line 1 in test/bugs/github1759.v

View workflow job for this annotation

GitHub Actions / opam-build (latest, ubuntu-latest) 

Cannot find a physical path bound to logical path Types.

Check failure on line 1 in test/bugs/github1759.v

View workflow job for this annotation

GitHub Actions / opam-build (dev, ubuntu-latest) 

Cannot find a physical path bound to logical path Types.
Require Import Spaces.No.

Section Foo.
Context {S : OptionSort@{i}}.
Notation GenNo := (GenNo S).
Local Open Scope surreal_scope.
Context
(A : GenNo -> Type)
(dle : forall (x y : GenNo), (x <= y) -> A x -> A y -> Type)
(dlt : forall (x y : GenNo), (x < y) -> A x -> A y -> Type)
{ishprop_le : forall x y a b p, IsHProp (dle x y p a b)}
{ishprop_lt : forall x y a b p, IsHProp (dlt x y p a b)}
(dcut : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r)),
A {{ xL | xR // xcut }})
(dcut' : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r)),
A {{ xL | xR // xcut }})
(dpath : forall (x y : GenNo) (a:A x) (b:A y) (p : x <= y) (q : y <= x)
(dp : dle x y p a b) (dq : dle y x q b a),
path_No _ _ p q # a = b)
(dle_lr : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r))
(L' R' : Type@{i}) (s' : InSort@{i} S L' R')
(yL : L' -> GenNo) (yR : R' -> GenNo)
(ycut : forall (l:L') (r:R'), (yL l) < (yR r))
(fyL : forall l, A (yL l)) (fyR : forall r, A (yR r))
(fycut : forall l r, dlt _ _ (ycut l r) (fyL l) (fyR r))
(p : forall (l:L), xL l < {{ yL | yR // ycut }})
(dp : forall (l:L),
dlt _ _ (p l)
(fxL l)
(dcut _ _ _ yL yR ycut fyL fyR fycut))
(q : forall (r:R'), {{ xL | xR // xcut }} < yR r)
(dq : forall (r:R'),
dlt _ _ (q r)
(dcut _ _ _ xL xR xcut fxL fxR fxcut)
(fyR r)),
dle {{ xL | xR // xcut }} {{ yL | yR // ycut }}
(le_lr xL xR xcut yL yR ycut p q)
(dcut _ _ _ xL xR xcut fxL fxR fxcut)
(dcut _ _ _ yL yR ycut fyL fyR fycut))
(dle_lr' : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r))
(L' R' : Type@{i}) (s' : InSort@{i} S L' R')
(yL : L' -> GenNo) (yR : R' -> GenNo)
(ycut : forall (l:L') (r:R'), (yL l) < (yR r))
(fyL : forall l, A (yL l)) (fyR : forall r, A (yR r))
(fycut : forall l r, dlt _ _ (ycut l r) (fyL l) (fyR r))
(p : forall (l:L), xL l < {{ yL | yR // ycut }})
(dp : forall (l:L),
dlt _ _ (p l)
(fxL l)
(dcut' _ _ _ yL yR ycut fyL fyR fycut))
(q : forall (r:R'), {{ xL | xR // xcut }} < yR r)
(dq : forall (r:R'),
dlt _ _ (q r)
(dcut' _ _ _ xL xR xcut fxL fxR fxcut)
(fyR r)),
dle {{ xL | xR // xcut }} {{ yL | yR // ycut }}
(le_lr xL xR xcut yL yR ycut p q)
(dcut' _ _ _ xL xR xcut fxL fxR fxcut)
(dcut' _ _ _ yL yR ycut fyL fyR fycut))
(dlt_l : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r))
(L' R' : Type@{i}) (s' : InSort@{i} S L' R')
(yL : L' -> GenNo) (yR : R' -> GenNo)
(ycut : forall (l:L') (r:R'), (yL l) < (yR r))
(fyL : forall l, A (yL l)) (fyR : forall r, A (yR r))
(fycut : forall l r, dlt _ _ (ycut l r) (fyL l) (fyR r))
(l : L')
(p : {{ xL | xR // xcut }} <= yL l)
(dp : dle _ _ p
(dcut _ _ _ xL xR xcut fxL fxR fxcut)
(fyL l)),
dlt {{ xL | xR // xcut }} {{ yL | yR // ycut }}
(lt_l xL xR xcut yL yR ycut l p)
(dcut _ _ _ xL xR xcut fxL fxR fxcut)
(dcut _ _ _ yL yR ycut fyL fyR fycut))
(dlt_l' : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r))
(L' R' : Type@{i}) (s' : InSort@{i} S L' R')
(yL : L' -> GenNo) (yR : R' -> GenNo)
(ycut : forall (l:L') (r:R'), (yL l) < (yR r))
(fyL : forall l, A (yL l)) (fyR : forall r, A (yR r))
(fycut : forall l r, dlt _ _ (ycut l r) (fyL l) (fyR r))
(l : L')
(p : {{ xL | xR // xcut }} <= yL l)
(dp : dle _ _ p
(dcut' _ _ _ xL xR xcut fxL fxR fxcut)
(fyL l)),
dlt {{ xL | xR // xcut }} {{ yL | yR // ycut }}
(lt_l xL xR xcut yL yR ycut l p)
(dcut' _ _ _ xL xR xcut fxL fxR fxcut)
(dcut' _ _ _ yL yR ycut fyL fyR fycut))
(dlt_r : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r))
(L' R' : Type@{i}) (s' : InSort@{i} S L' R')
(yL : L' -> GenNo) (yR : R' -> GenNo)
(ycut : forall (l:L') (r:R'), (yL l) < (yR r))
(fyL : forall l, A (yL l)) (fyR : forall r, A (yR r))
(fycut : forall l r, dlt _ _ (ycut l r) (fyL l) (fyR r))
(r : R)
(p : (xR r) <= {{ yL | yR // ycut }})
(dp : dle _ _ p
(fxR r)
(dcut _ _ _ yL yR ycut fyL fyR fycut)),
dlt {{ xL | xR // xcut }} {{ yL | yR // ycut }}
(lt_r xL xR xcut yL yR ycut r p)
(dcut _ _ _ xL xR xcut fxL fxR fxcut)
(dcut _ _ _ yL yR ycut fyL fyR fycut))
(dlt_r' : forall (L R : Type@{i}) (s : InSort@{i} S L R)
(xL : L -> GenNo) (xR : R -> GenNo)
(xcut : forall (l:L) (r:R), (xL l) < (xR r))
(fxL : forall l, A (xL l)) (fxR : forall r, A (xR r))
(fxcut : forall l r, dlt _ _ (xcut l r) (fxL l) (fxR r))
(L' R' : Type@{i}) (s' : InSort@{i} S L' R')
(yL : L' -> GenNo) (yR : R' -> GenNo)
(ycut : forall (l:L') (r:R'), (yL l) < (yR r))
(fyL : forall l, A (yL l)) (fyR : forall r, A (yR r))
(fycut : forall l r, dlt _ _ (ycut l r) (fyL l) (fyR r))
(r : R)
(p : (xR r) <= {{ yL | yR // ycut }})
(dp : dle _ _ p
(fxR r)
(dcut' _ _ _ yL yR ycut fyL fyR fycut)),
dlt {{ xL | xR // xcut }} {{ yL | yR // ycut }}
(lt_r xL xR xcut yL yR ycut r p)
(dcut' _ _ _ xL xR xcut fxL fxR fxcut)
(dcut' _ _ _ yL yR ycut fyL fyR fycut)).

Definition foo : forall x, A x
:= No_ind A dle dlt dcut dpath dle_lr dlt_l dlt_r.

Definition bar : forall x, A x
:= No_ind A dle dlt dcut' dpath dle_lr' dlt_l' dlt_r'.

Fail Definition foobar
: forall x, foo x = bar x
:= 1.

End Foo.
2 changes: 2 additions & 0 deletions theories/Spaces/No/Core.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,9 @@ Finally, for conceptual isolation, and so as not to depend on the particular imp

Definition No_ind (x : GenNo) : A x.
Proof.
revert dle dlt ishprop_le ishprop_lt dcut dpath dle_lr dlt_l dlt_r.
destruct x as [x xno].
intros dle dlt ishprop_le ishprop_lt dcut dpath dle_lr dlt_l dlt_r.
exact (No_ind_internal x xno).
Defined.

Expand Down

0 comments on commit 198772b

Please sign in to comment.