New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Circumvention of forcing analysis brings back easy proof of Fin injectivity #1427

Closed
GoogleCodeExporter opened this Issue Aug 8, 2015 · 5 comments

Comments

Projects
None yet
3 participants
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

Continuing issue #1406: one can circumvent the forcing analysis by parametrization:

open import Common.Equality
open import Common.Prelude

data HEq (A : Set) (a : A) : (B : Set) (b : B) → Set1 where
  refl : HEq A a A a

-- Parametrizing over the natural numbers circumvents the forcing analysis.

module F (N : Set) (s : NN) where

  data Fin : (n : N) → Set where
    zero : {n : N}              Fin (s n)
    suc  : {n : N} (i : Fin n)  Fin (s n)

open F Nat suc

inj-Fin-≅ :  {n m} {i : Fin n} {j : Fin m}  HEq (Fin n) i (Fin m) j  
n ≡ m
inj-Fin-≅ {i = zero}  {zero  } refl = refl  -- Expected to fail, as n /= m
inj-Fin-≅ {i = zero}  {suc  j} ()
inj-Fin-≅ {i = suc i} {zero  } ()
inj-Fin-≅ {i = suc i} {suc .i} refl = refl  -- Expected to fail, as n /= m

-- This should no longer be accepted, as the direct attempt also fails:

inj-Fin-≅' :  {n m} {i : Fin n} {j : Fin m}  HEq (Fin n) i (Fin m) j 
→ n ≡ m
inj-Fin-≅' refl = refl

Seems like to really fix heterogeneous equality, we need to reopen issue #292.

Original issue reported on code.google.com by andreas....@gmail.com on 10 Feb 2015 at 7:22

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Nisse reports that my fix of issue #1406 makes some proofs by pattern matching much harder.

Either the fix for issue 1406 has to be restricted to big forced arguments introduced by 9a4ebdd or we have to roll back that feature by Ulf.

Ideally, we will properly solve heterogeneous matching (with a solid theoretical foundation).

This issue is release-blocking.

Original comment by andreas....@gmail.com on 15 Feb 2015 at 9:27

  • Added labels: Milestone-2.4.2.3, Priority-High
  • Removed labels: Priority-Medium
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Labeled as critical since issue is a release-blocking.

Original comment by andres.s...@gmail.com on 15 Feb 2015 at 2:57

  • Added labels: Priority-Critical
  • Removed labels: Priority-High
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andres.s...@gmail.com on 16 Feb 2015 at 10:53

  • Added labels: Priority-Highest
  • Removed labels: Priority-Critical
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 24 Feb 2015 at 6:40

  • Added labels: Forcing
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Implemented comment 1 in 5e9ec5f

Original comment by andreas....@gmail.com on 27 Feb 2015 at 8:10

  • Changed state: Fixed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment