641a4548b6
The `no_confusion` construction is only generated for inductive datatypes supported in the kernel. Before this commit, given `h : T`, `cases h` could leak the internal encoding used by the inductive compiler WHEN a nested and/or mutual inductive datatype is used to index the inductive datatype `T`. The new test exposes the problem. The solution implemented in this commit uses inj_arrow lemmas generated by the inductive compiler. We only use the lemmas if the target is a proposition. If it is not, we sign an error. The reason for this limitation is documented in the source code. cc @jroesch @dselsam Jared: the information leakage has been fixed. So, students will not be confused by the internal encoding used in the inductive compiler. I added the example I posted on slack as a new test. Note that, the workaround I used has been removed.
37 lines
1.3 KiB
Text
37 lines
1.3 KiB
Text
t₁ : term,
|
|
c₁ c₂ : string,
|
|
h₁ h₂ : is_rename (term.const c₁) c₁ c₂ (term.const c₂)
|
|
⊢ term.const c₂ = term.const c₂
|
|
t₁ : term,
|
|
c₁ c₂ : string,
|
|
h₁ : is_rename (term.const c₁) c₁ c₂ (term.const c₂),
|
|
hne : c₁ ≠ c₁,
|
|
h₂ : is_rename (term.const c₁) c₁ c₂ (term.const c₁)
|
|
⊢ term.const c₂ = term.const c₁
|
|
t₁ : term,
|
|
c₁ c₂ : string,
|
|
hne : c₁ ≠ c₁,
|
|
h₁ : is_rename (term.const c₁) c₁ c₂ (term.const c₁),
|
|
h₂ : is_rename (term.const c₁) c₁ c₂ (term.const c₂)
|
|
⊢ term.const c₁ = term.const c₂
|
|
t₁ : term,
|
|
c₁ c₁' c₂ : string,
|
|
hne : c₁ ≠ c₁',
|
|
h₁ : is_rename (term.const c₁) c₁' c₂ (term.const c₁),
|
|
hne_1 : c₁ ≠ c₁',
|
|
h₂ : is_rename (term.const c₁) c₁' c₂ (term.const c₁)
|
|
⊢ term.const c₁ = term.const c₁
|
|
t₁ : term,
|
|
fn : string,
|
|
ts : list term,
|
|
ih :
|
|
∀ (ts₂ ts₂' : list term) (c₁ c₂ : string),
|
|
is_rename_lst ts c₁ c₂ ts₂ → is_rename_lst ts c₁ c₂ ts₂' → ts₂ = ts₂',
|
|
c₁ c₂ : string,
|
|
ts₂ : list term,
|
|
h₁_1 : is_rename_lst ts c₁ c₂ ts₂,
|
|
h₁ : is_rename (term.app fn ts) c₁ c₂ (term.app fn ts₂),
|
|
ts₂_1 : list term,
|
|
h₁_2 : is_rename_lst ts c₁ c₂ ts₂_1,
|
|
h₂ : is_rename (term.app fn ts) c₁ c₂ (term.app fn ts₂_1)
|
|
⊢ term.app fn ts₂ = term.app fn ts₂_1
|