Zulip Chat Archive

Stream: new members

Topic: Unfold a cast expression


view this post on Zulip Oskar Berndal (Jan 15 2021 at 23:52):

How can I simplify/unfold a cast expression? Below should illustrate an example of what I mean.

import data.nat.parity

inductive parity
| even : parity
| odd : parity

def suitable : parity    Prop
| parity.even n := (n%2 = 0)
| parity.odd  n := (n%2 = 1)

def pa_nat (σ : parity) := {n :  // suitable σ n}

def pa_nat_to_nat {σ : parity} : pa_nat σ  
| n, _ := n

instance pa_nat_to_nat_coe {σ : parity} : has_coe (pa_nat σ)  :=
 pa_nat_to_nat 

def opaque_function :     
| n m := n + m

lemma apply_opaque_function {σ σ' : parity} :   (n : pa_nat σ) (m : pa_nat σ'), σ  σ'  (opaque_function n m)%2 = 1
| n, p m, q neq :=
begin
  sorry --how to unfold the casts?
end

I know that I can use the change tactic to say what I want the goal to be but that is quite cumbersome in my use case and it feels like there should be a way that 'uses' the casts.

view this post on Zulip Johan Commelin (Jan 16 2021 at 04:03):

@Oskar Berndal unfold_coes is a tactic made exactly for this job :smiley:

view this post on Zulip Oskar Berndal (Jan 16 2021 at 10:52):

Indeed it did! Many thanks ^___^


Last updated: May 14 2021 at 07:19 UTC